0 Prolog
↳1 PrologToDTProblemTransformerProof (⇒, 383 ms)
↳2 TRIPLES
↳3 TriplesToPiDPProof (⇒, 358 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 PiDP
↳10 PiDPToQDPProof (⇒, 0 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 0 ms)
↳13 YES
↳14 PiDP
↳15 UsableRulesProof (⇔, 0 ms)
↳16 PiDP
↳17 PiDPToQDPProof (⇒, 0 ms)
↳18 QDP
↳19 QDPSizeChangeProof (⇔, 0 ms)
↳20 YES
↳21 PiDP
↳22 UsableRulesProof (⇔, 0 ms)
↳23 PiDP
↳24 PiDPToQDPProof (⇒, 0 ms)
↳25 QDP
↳26 QDPSizeChangeProof (⇔, 0 ms)
↳27 YES
↳28 PiDP
↳29 UsableRulesProof (⇔, 0 ms)
↳30 PiDP
↳31 PiDPToQDPProof (⇒, 0 ms)
↳32 QDP
↳33 QDPSizeChangeProof (⇔, 0 ms)
↳34 YES
↳35 PiDP
↳36 UsableRulesProof (⇔, 0 ms)
↳37 PiDP
↳38 PiDPToQDPProof (⇒, 0 ms)
↳39 QDP
↳40 Narrowing (⇒, 0 ms)
↳41 QDP
↳42 UsableRulesProof (⇔, 0 ms)
↳43 QDP
↳44 QReductionProof (⇔, 0 ms)
↳45 QDP
↳46 Instantiation (⇔, 0 ms)
↳47 QDP
↳48 DependencyGraphProof (⇔, 0 ms)
↳49 QDP
↳50 QDPQMonotonicMRRProof (⇔, 1118 ms)
↳51 QDP
↳52 QDPQMonotonicMRRProof (⇔, 1200 ms)
↳53 QDP
↳54 QDPOrderProof (⇔, 160 ms)
↳55 QDP
↳56 DependencyGraphProof (⇔, 0 ms)
↳57 QDP
↳58 UsableRulesProof (⇔, 0 ms)
↳59 QDP
↳60 QReductionProof (⇔, 0 ms)
↳61 QDP
↳62 QDPQMonotonicMRRProof (⇔, 528 ms)
↳63 QDP
↳64 QDPOrderProof (⇔, 222 ms)
↳65 QDP
↳66 DependencyGraphProof (⇔, 0 ms)
↳67 QDP
↳68 UsableRulesProof (⇔, 0 ms)
↳69 QDP
↳70 QReductionProof (⇔, 0 ms)
↳71 QDP
↳72 QDPQMonotonicMRRProof (⇔, 1805 ms)
↳73 QDP
↳74 DependencyGraphProof (⇔, 0 ms)
↳75 QDP
↳76 UsableRulesProof (⇔, 0 ms)
↳77 QDP
↳78 QReductionProof (⇔, 2 ms)
↳79 QDP
↳80 QDPQMonotonicMRRProof (⇔, 407 ms)
↳81 QDP
↳82 UsableRulesProof (⇔, 0 ms)
↳83 QDP
↳84 QReductionProof (⇔, 0 ms)
↳85 QDP
↳86 Narrowing (⇒, 0 ms)
↳87 QDP
↳88 UsableRulesProof (⇔, 0 ms)
↳89 QDP
↳90 QReductionProof (⇔, 0 ms)
↳91 QDP
↳92 Instantiation (⇔, 0 ms)
↳93 QDP
↳94 MRRProof (⇔, 23 ms)
↳95 QDP
↳96 PisEmptyProof (⇔, 0 ms)
↳97 YES
MAXSORTA_IN_GA(.(X1, []), .(X1, X2)) → U7_GA(X1, X2, delcB_in_ga(X1, X3))
U7_GA(X1, X2, delcB_out_ga(X1, X3)) → U8_GA(X1, X2, maxsortA_in_ga(X3, X2))
U7_GA(X1, X2, delcB_out_ga(X1, X3)) → MAXSORTA_IN_GA(X3, X2)
MAXSORTA_IN_GA(.(t, .(t, X1)), .(X2, X3)) → U9_GA(X1, X2, X3, maxC_in_ga(X1, X2))
MAXSORTA_IN_GA(.(t, .(t, X1)), .(X2, X3)) → MAXC_IN_GA(X1, X2)
MAXC_IN_GA(.(t, X1), X2) → U1_GA(X1, X2, maxC_in_ga(X1, X2))
MAXC_IN_GA(.(t, X1), X2) → MAXC_IN_GA(X1, X2)
MAXC_IN_GA(.(f, X1), X2) → U2_GA(X1, X2, maxC_in_ga(X1, X2))
MAXC_IN_GA(.(f, X1), X2) → MAXC_IN_GA(X1, X2)
MAXSORTA_IN_GA(.(t, .(t, X1)), .(f, X2)) → U10_GA(X1, X2, maxcC_in_gg(X1, f))
U10_GA(X1, X2, maxcC_out_gg(X1, f)) → U11_GA(X1, X2, delI_in_ga(X1, X3))
U10_GA(X1, X2, maxcC_out_gg(X1, f)) → DELI_IN_GA(X1, X3)
DELI_IN_GA(.(t, X1), .(t, X2)) → U3_GA(X1, X2, delI_in_ga(X1, X2))
DELI_IN_GA(.(t, X1), .(t, X2)) → DELI_IN_GA(X1, X2)
MAXSORTA_IN_GA(.(t, .(t, X1)), .(X2, X3)) → U12_GA(X1, X2, X3, maxcC_in_ga(X1, X2))
U12_GA(X1, X2, X3, maxcC_out_ga(X1, X2)) → U13_GA(X1, X2, X3, delcD_in_gga(X2, X1, X4))
U13_GA(X1, X2, X3, delcD_out_gga(X2, X1, X4)) → U14_GA(X1, X2, X3, maxsortA_in_ga(X4, X3))
U13_GA(X1, X2, X3, delcD_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4, X3)
MAXSORTA_IN_GA(.(t, .(f, X1)), .(X2, X3)) → U15_GA(X1, X2, X3, maxC_in_ga(X1, X2))
MAXSORTA_IN_GA(.(t, .(f, X1)), .(X2, X3)) → MAXC_IN_GA(X1, X2)
MAXSORTA_IN_GA(.(t, .(f, X1)), .(f, X2)) → U16_GA(X1, X2, maxcC_in_gg(X1, f))
U16_GA(X1, X2, maxcC_out_gg(X1, f)) → U17_GA(X1, X2, delI_in_ga(.(f, X1), X3))
U16_GA(X1, X2, maxcC_out_gg(X1, f)) → DELI_IN_GA(.(f, X1), X3)
MAXSORTA_IN_GA(.(t, .(f, X1)), .(X2, X3)) → U18_GA(X1, X2, X3, maxcC_in_ga(X1, X2))
U18_GA(X1, X2, X3, maxcC_out_ga(X1, X2)) → U19_GA(X1, X2, X3, delcE_in_gga(X2, X1, X4))
U19_GA(X1, X2, X3, delcE_out_gga(X2, X1, X4)) → U20_GA(X1, X2, X3, maxsortA_in_ga(X4, X3))
U19_GA(X1, X2, X3, delcE_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4, X3)
MAXSORTA_IN_GA(.(f, .(f, X1)), .(X2, X3)) → U21_GA(X1, X2, X3, maxF_in_ga(X1, X2))
MAXSORTA_IN_GA(.(f, .(f, X1)), .(X2, X3)) → MAXF_IN_GA(X1, X2)
MAXF_IN_GA(.(f, X1), X2) → U4_GA(X1, X2, maxF_in_ga(X1, X2))
MAXF_IN_GA(.(f, X1), X2) → MAXF_IN_GA(X1, X2)
MAXF_IN_GA(.(t, X1), X2) → U5_GA(X1, X2, maxC_in_ga(X1, X2))
MAXF_IN_GA(.(t, X1), X2) → MAXC_IN_GA(X1, X2)
MAXSORTA_IN_GA(.(f, .(f, X1)), .(t, X2)) → U22_GA(X1, X2, maxcF_in_gg(X1, t))
U22_GA(X1, X2, maxcF_out_gg(X1, t)) → U23_GA(X1, X2, delJ_in_ga(X1, X3))
U22_GA(X1, X2, maxcF_out_gg(X1, t)) → DELJ_IN_GA(X1, X3)
DELJ_IN_GA(.(f, X1), .(f, X2)) → U6_GA(X1, X2, delJ_in_ga(X1, X2))
DELJ_IN_GA(.(f, X1), .(f, X2)) → DELJ_IN_GA(X1, X2)
MAXSORTA_IN_GA(.(f, .(f, X1)), .(X2, X3)) → U24_GA(X1, X2, X3, maxcF_in_ga(X1, X2))
U24_GA(X1, X2, X3, maxcF_out_ga(X1, X2)) → U25_GA(X1, X2, X3, delcG_in_gga(X2, X1, X4))
U25_GA(X1, X2, X3, delcG_out_gga(X2, X1, X4)) → U26_GA(X1, X2, X3, maxsortA_in_ga(X4, X3))
U25_GA(X1, X2, X3, delcG_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4, X3)
MAXSORTA_IN_GA(.(f, .(t, X1)), .(X2, X3)) → U27_GA(X1, X2, X3, maxC_in_ga(X1, X2))
MAXSORTA_IN_GA(.(f, .(t, X1)), .(X2, X3)) → MAXC_IN_GA(X1, X2)
MAXSORTA_IN_GA(.(f, .(t, X1)), .(t, X2)) → U28_GA(X1, X2, maxcC_in_gg(X1, t))
U28_GA(X1, X2, maxcC_out_gg(X1, t)) → U29_GA(X1, X2, delJ_in_ga(.(t, X1), X3))
U28_GA(X1, X2, maxcC_out_gg(X1, t)) → DELJ_IN_GA(.(t, X1), X3)
MAXSORTA_IN_GA(.(f, .(t, X1)), .(X2, X3)) → U30_GA(X1, X2, X3, maxcC_in_ga(X1, X2))
U30_GA(X1, X2, X3, maxcC_out_ga(X1, X2)) → U31_GA(X1, X2, X3, delcH_in_gga(X2, X1, X4))
U31_GA(X1, X2, X3, delcH_out_gga(X2, X1, X4)) → U32_GA(X1, X2, X3, maxsortA_in_ga(X4, X3))
U31_GA(X1, X2, X3, delcH_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4, X3)
delcB_in_ga(t, []) → delcB_out_ga(t, [])
delcB_in_ga(f, []) → delcB_out_ga(f, [])
maxcC_in_gg([], t) → maxcC_out_gg([], t)
maxcC_in_gg(.(t, X1), X2) → U48_gg(X1, X2, maxcC_in_gg(X1, X2))
maxcC_in_gg(.(f, X1), X2) → U49_gg(X1, X2, maxcC_in_gg(X1, X2))
U49_gg(X1, X2, maxcC_out_gg(X1, X2)) → maxcC_out_gg(.(f, X1), X2)
U48_gg(X1, X2, maxcC_out_gg(X1, X2)) → maxcC_out_gg(.(t, X1), X2)
maxcC_in_ga([], t) → maxcC_out_ga([], t)
maxcC_in_ga(.(t, X1), X2) → U48_ga(X1, X2, maxcC_in_ga(X1, X2))
maxcC_in_ga(.(f, X1), X2) → U49_ga(X1, X2, maxcC_in_ga(X1, X2))
U49_ga(X1, X2, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(f, X1), X2)
U48_ga(X1, X2, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(t, X1), X2)
delcD_in_gga(t, X1, .(t, X1)) → delcD_out_gga(t, X1, .(t, X1))
delcD_in_gga(f, X1, .(t, .(t, X2))) → U54_gga(X1, X2, delcI_in_ga(X1, X2))
delcI_in_ga([], []) → delcI_out_ga([], [])
delcI_in_ga(.(f, X1), X1) → delcI_out_ga(.(f, X1), X1)
delcI_in_ga(.(t, X1), .(t, X2)) → U50_ga(X1, X2, delcI_in_ga(X1, X2))
U50_ga(X1, X2, delcI_out_ga(X1, X2)) → delcI_out_ga(.(t, X1), .(t, X2))
U54_gga(X1, X2, delcI_out_ga(X1, X2)) → delcD_out_gga(f, X1, .(t, .(t, X2)))
delcE_in_gga(t, X1, .(f, X1)) → delcE_out_gga(t, X1, .(f, X1))
delcE_in_gga(f, X1, .(t, X2)) → U55_gga(X1, X2, delcI_in_ga(.(f, X1), X2))
U55_gga(X1, X2, delcI_out_ga(.(f, X1), X2)) → delcE_out_gga(f, X1, .(t, X2))
maxcF_in_gg([], f) → maxcF_out_gg([], f)
maxcF_in_gg(.(f, X1), X2) → U51_gg(X1, X2, maxcF_in_gg(X1, X2))
maxcF_in_gg(.(t, X1), X2) → U52_gg(X1, X2, maxcC_in_gg(X1, X2))
U52_gg(X1, X2, maxcC_out_gg(X1, X2)) → maxcF_out_gg(.(t, X1), X2)
U51_gg(X1, X2, maxcF_out_gg(X1, X2)) → maxcF_out_gg(.(f, X1), X2)
maxcF_in_ga([], f) → maxcF_out_ga([], f)
maxcF_in_ga(.(f, X1), X2) → U51_ga(X1, X2, maxcF_in_ga(X1, X2))
maxcF_in_ga(.(t, X1), X2) → U52_ga(X1, X2, maxcC_in_ga(X1, X2))
U52_ga(X1, X2, maxcC_out_ga(X1, X2)) → maxcF_out_ga(.(t, X1), X2)
U51_ga(X1, X2, maxcF_out_ga(X1, X2)) → maxcF_out_ga(.(f, X1), X2)
delcG_in_gga(f, X1, .(f, X1)) → delcG_out_gga(f, X1, .(f, X1))
delcG_in_gga(t, X1, .(f, .(f, X2))) → U56_gga(X1, X2, delcJ_in_ga(X1, X2))
delcJ_in_ga([], []) → delcJ_out_ga([], [])
delcJ_in_ga(.(t, X1), X1) → delcJ_out_ga(.(t, X1), X1)
delcJ_in_ga(.(f, X1), .(f, X2)) → U53_ga(X1, X2, delcJ_in_ga(X1, X2))
U53_ga(X1, X2, delcJ_out_ga(X1, X2)) → delcJ_out_ga(.(f, X1), .(f, X2))
U56_gga(X1, X2, delcJ_out_ga(X1, X2)) → delcG_out_gga(t, X1, .(f, .(f, X2)))
delcH_in_gga(f, X1, .(t, X1)) → delcH_out_gga(f, X1, .(t, X1))
delcH_in_gga(t, X1, .(f, X2)) → U57_gga(X1, X2, delcJ_in_ga(.(t, X1), X2))
U57_gga(X1, X2, delcJ_out_ga(.(t, X1), X2)) → delcH_out_gga(t, X1, .(f, X2))
Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES
MAXSORTA_IN_GA(.(X1, []), .(X1, X2)) → U7_GA(X1, X2, delcB_in_ga(X1, X3))
U7_GA(X1, X2, delcB_out_ga(X1, X3)) → U8_GA(X1, X2, maxsortA_in_ga(X3, X2))
U7_GA(X1, X2, delcB_out_ga(X1, X3)) → MAXSORTA_IN_GA(X3, X2)
MAXSORTA_IN_GA(.(t, .(t, X1)), .(X2, X3)) → U9_GA(X1, X2, X3, maxC_in_ga(X1, X2))
MAXSORTA_IN_GA(.(t, .(t, X1)), .(X2, X3)) → MAXC_IN_GA(X1, X2)
MAXC_IN_GA(.(t, X1), X2) → U1_GA(X1, X2, maxC_in_ga(X1, X2))
MAXC_IN_GA(.(t, X1), X2) → MAXC_IN_GA(X1, X2)
MAXC_IN_GA(.(f, X1), X2) → U2_GA(X1, X2, maxC_in_ga(X1, X2))
MAXC_IN_GA(.(f, X1), X2) → MAXC_IN_GA(X1, X2)
MAXSORTA_IN_GA(.(t, .(t, X1)), .(f, X2)) → U10_GA(X1, X2, maxcC_in_gg(X1, f))
U10_GA(X1, X2, maxcC_out_gg(X1, f)) → U11_GA(X1, X2, delI_in_ga(X1, X3))
U10_GA(X1, X2, maxcC_out_gg(X1, f)) → DELI_IN_GA(X1, X3)
DELI_IN_GA(.(t, X1), .(t, X2)) → U3_GA(X1, X2, delI_in_ga(X1, X2))
DELI_IN_GA(.(t, X1), .(t, X2)) → DELI_IN_GA(X1, X2)
MAXSORTA_IN_GA(.(t, .(t, X1)), .(X2, X3)) → U12_GA(X1, X2, X3, maxcC_in_ga(X1, X2))
U12_GA(X1, X2, X3, maxcC_out_ga(X1, X2)) → U13_GA(X1, X2, X3, delcD_in_gga(X2, X1, X4))
U13_GA(X1, X2, X3, delcD_out_gga(X2, X1, X4)) → U14_GA(X1, X2, X3, maxsortA_in_ga(X4, X3))
U13_GA(X1, X2, X3, delcD_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4, X3)
MAXSORTA_IN_GA(.(t, .(f, X1)), .(X2, X3)) → U15_GA(X1, X2, X3, maxC_in_ga(X1, X2))
MAXSORTA_IN_GA(.(t, .(f, X1)), .(X2, X3)) → MAXC_IN_GA(X1, X2)
MAXSORTA_IN_GA(.(t, .(f, X1)), .(f, X2)) → U16_GA(X1, X2, maxcC_in_gg(X1, f))
U16_GA(X1, X2, maxcC_out_gg(X1, f)) → U17_GA(X1, X2, delI_in_ga(.(f, X1), X3))
U16_GA(X1, X2, maxcC_out_gg(X1, f)) → DELI_IN_GA(.(f, X1), X3)
MAXSORTA_IN_GA(.(t, .(f, X1)), .(X2, X3)) → U18_GA(X1, X2, X3, maxcC_in_ga(X1, X2))
U18_GA(X1, X2, X3, maxcC_out_ga(X1, X2)) → U19_GA(X1, X2, X3, delcE_in_gga(X2, X1, X4))
U19_GA(X1, X2, X3, delcE_out_gga(X2, X1, X4)) → U20_GA(X1, X2, X3, maxsortA_in_ga(X4, X3))
U19_GA(X1, X2, X3, delcE_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4, X3)
MAXSORTA_IN_GA(.(f, .(f, X1)), .(X2, X3)) → U21_GA(X1, X2, X3, maxF_in_ga(X1, X2))
MAXSORTA_IN_GA(.(f, .(f, X1)), .(X2, X3)) → MAXF_IN_GA(X1, X2)
MAXF_IN_GA(.(f, X1), X2) → U4_GA(X1, X2, maxF_in_ga(X1, X2))
MAXF_IN_GA(.(f, X1), X2) → MAXF_IN_GA(X1, X2)
MAXF_IN_GA(.(t, X1), X2) → U5_GA(X1, X2, maxC_in_ga(X1, X2))
MAXF_IN_GA(.(t, X1), X2) → MAXC_IN_GA(X1, X2)
MAXSORTA_IN_GA(.(f, .(f, X1)), .(t, X2)) → U22_GA(X1, X2, maxcF_in_gg(X1, t))
U22_GA(X1, X2, maxcF_out_gg(X1, t)) → U23_GA(X1, X2, delJ_in_ga(X1, X3))
U22_GA(X1, X2, maxcF_out_gg(X1, t)) → DELJ_IN_GA(X1, X3)
DELJ_IN_GA(.(f, X1), .(f, X2)) → U6_GA(X1, X2, delJ_in_ga(X1, X2))
DELJ_IN_GA(.(f, X1), .(f, X2)) → DELJ_IN_GA(X1, X2)
MAXSORTA_IN_GA(.(f, .(f, X1)), .(X2, X3)) → U24_GA(X1, X2, X3, maxcF_in_ga(X1, X2))
U24_GA(X1, X2, X3, maxcF_out_ga(X1, X2)) → U25_GA(X1, X2, X3, delcG_in_gga(X2, X1, X4))
U25_GA(X1, X2, X3, delcG_out_gga(X2, X1, X4)) → U26_GA(X1, X2, X3, maxsortA_in_ga(X4, X3))
U25_GA(X1, X2, X3, delcG_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4, X3)
MAXSORTA_IN_GA(.(f, .(t, X1)), .(X2, X3)) → U27_GA(X1, X2, X3, maxC_in_ga(X1, X2))
MAXSORTA_IN_GA(.(f, .(t, X1)), .(X2, X3)) → MAXC_IN_GA(X1, X2)
MAXSORTA_IN_GA(.(f, .(t, X1)), .(t, X2)) → U28_GA(X1, X2, maxcC_in_gg(X1, t))
U28_GA(X1, X2, maxcC_out_gg(X1, t)) → U29_GA(X1, X2, delJ_in_ga(.(t, X1), X3))
U28_GA(X1, X2, maxcC_out_gg(X1, t)) → DELJ_IN_GA(.(t, X1), X3)
MAXSORTA_IN_GA(.(f, .(t, X1)), .(X2, X3)) → U30_GA(X1, X2, X3, maxcC_in_ga(X1, X2))
U30_GA(X1, X2, X3, maxcC_out_ga(X1, X2)) → U31_GA(X1, X2, X3, delcH_in_gga(X2, X1, X4))
U31_GA(X1, X2, X3, delcH_out_gga(X2, X1, X4)) → U32_GA(X1, X2, X3, maxsortA_in_ga(X4, X3))
U31_GA(X1, X2, X3, delcH_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4, X3)
delcB_in_ga(t, []) → delcB_out_ga(t, [])
delcB_in_ga(f, []) → delcB_out_ga(f, [])
maxcC_in_gg([], t) → maxcC_out_gg([], t)
maxcC_in_gg(.(t, X1), X2) → U48_gg(X1, X2, maxcC_in_gg(X1, X2))
maxcC_in_gg(.(f, X1), X2) → U49_gg(X1, X2, maxcC_in_gg(X1, X2))
U49_gg(X1, X2, maxcC_out_gg(X1, X2)) → maxcC_out_gg(.(f, X1), X2)
U48_gg(X1, X2, maxcC_out_gg(X1, X2)) → maxcC_out_gg(.(t, X1), X2)
maxcC_in_ga([], t) → maxcC_out_ga([], t)
maxcC_in_ga(.(t, X1), X2) → U48_ga(X1, X2, maxcC_in_ga(X1, X2))
maxcC_in_ga(.(f, X1), X2) → U49_ga(X1, X2, maxcC_in_ga(X1, X2))
U49_ga(X1, X2, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(f, X1), X2)
U48_ga(X1, X2, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(t, X1), X2)
delcD_in_gga(t, X1, .(t, X1)) → delcD_out_gga(t, X1, .(t, X1))
delcD_in_gga(f, X1, .(t, .(t, X2))) → U54_gga(X1, X2, delcI_in_ga(X1, X2))
delcI_in_ga([], []) → delcI_out_ga([], [])
delcI_in_ga(.(f, X1), X1) → delcI_out_ga(.(f, X1), X1)
delcI_in_ga(.(t, X1), .(t, X2)) → U50_ga(X1, X2, delcI_in_ga(X1, X2))
U50_ga(X1, X2, delcI_out_ga(X1, X2)) → delcI_out_ga(.(t, X1), .(t, X2))
U54_gga(X1, X2, delcI_out_ga(X1, X2)) → delcD_out_gga(f, X1, .(t, .(t, X2)))
delcE_in_gga(t, X1, .(f, X1)) → delcE_out_gga(t, X1, .(f, X1))
delcE_in_gga(f, X1, .(t, X2)) → U55_gga(X1, X2, delcI_in_ga(.(f, X1), X2))
U55_gga(X1, X2, delcI_out_ga(.(f, X1), X2)) → delcE_out_gga(f, X1, .(t, X2))
maxcF_in_gg([], f) → maxcF_out_gg([], f)
maxcF_in_gg(.(f, X1), X2) → U51_gg(X1, X2, maxcF_in_gg(X1, X2))
maxcF_in_gg(.(t, X1), X2) → U52_gg(X1, X2, maxcC_in_gg(X1, X2))
U52_gg(X1, X2, maxcC_out_gg(X1, X2)) → maxcF_out_gg(.(t, X1), X2)
U51_gg(X1, X2, maxcF_out_gg(X1, X2)) → maxcF_out_gg(.(f, X1), X2)
maxcF_in_ga([], f) → maxcF_out_ga([], f)
maxcF_in_ga(.(f, X1), X2) → U51_ga(X1, X2, maxcF_in_ga(X1, X2))
maxcF_in_ga(.(t, X1), X2) → U52_ga(X1, X2, maxcC_in_ga(X1, X2))
U52_ga(X1, X2, maxcC_out_ga(X1, X2)) → maxcF_out_ga(.(t, X1), X2)
U51_ga(X1, X2, maxcF_out_ga(X1, X2)) → maxcF_out_ga(.(f, X1), X2)
delcG_in_gga(f, X1, .(f, X1)) → delcG_out_gga(f, X1, .(f, X1))
delcG_in_gga(t, X1, .(f, .(f, X2))) → U56_gga(X1, X2, delcJ_in_ga(X1, X2))
delcJ_in_ga([], []) → delcJ_out_ga([], [])
delcJ_in_ga(.(t, X1), X1) → delcJ_out_ga(.(t, X1), X1)
delcJ_in_ga(.(f, X1), .(f, X2)) → U53_ga(X1, X2, delcJ_in_ga(X1, X2))
U53_ga(X1, X2, delcJ_out_ga(X1, X2)) → delcJ_out_ga(.(f, X1), .(f, X2))
U56_gga(X1, X2, delcJ_out_ga(X1, X2)) → delcG_out_gga(t, X1, .(f, .(f, X2)))
delcH_in_gga(f, X1, .(t, X1)) → delcH_out_gga(f, X1, .(t, X1))
delcH_in_gga(t, X1, .(f, X2)) → U57_gga(X1, X2, delcJ_in_ga(.(t, X1), X2))
U57_gga(X1, X2, delcJ_out_ga(.(t, X1), X2)) → delcH_out_gga(t, X1, .(f, X2))
DELJ_IN_GA(.(f, X1), .(f, X2)) → DELJ_IN_GA(X1, X2)
delcB_in_ga(t, []) → delcB_out_ga(t, [])
delcB_in_ga(f, []) → delcB_out_ga(f, [])
maxcC_in_gg([], t) → maxcC_out_gg([], t)
maxcC_in_gg(.(t, X1), X2) → U48_gg(X1, X2, maxcC_in_gg(X1, X2))
maxcC_in_gg(.(f, X1), X2) → U49_gg(X1, X2, maxcC_in_gg(X1, X2))
U49_gg(X1, X2, maxcC_out_gg(X1, X2)) → maxcC_out_gg(.(f, X1), X2)
U48_gg(X1, X2, maxcC_out_gg(X1, X2)) → maxcC_out_gg(.(t, X1), X2)
maxcC_in_ga([], t) → maxcC_out_ga([], t)
maxcC_in_ga(.(t, X1), X2) → U48_ga(X1, X2, maxcC_in_ga(X1, X2))
maxcC_in_ga(.(f, X1), X2) → U49_ga(X1, X2, maxcC_in_ga(X1, X2))
U49_ga(X1, X2, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(f, X1), X2)
U48_ga(X1, X2, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(t, X1), X2)
delcD_in_gga(t, X1, .(t, X1)) → delcD_out_gga(t, X1, .(t, X1))
delcD_in_gga(f, X1, .(t, .(t, X2))) → U54_gga(X1, X2, delcI_in_ga(X1, X2))
delcI_in_ga([], []) → delcI_out_ga([], [])
delcI_in_ga(.(f, X1), X1) → delcI_out_ga(.(f, X1), X1)
delcI_in_ga(.(t, X1), .(t, X2)) → U50_ga(X1, X2, delcI_in_ga(X1, X2))
U50_ga(X1, X2, delcI_out_ga(X1, X2)) → delcI_out_ga(.(t, X1), .(t, X2))
U54_gga(X1, X2, delcI_out_ga(X1, X2)) → delcD_out_gga(f, X1, .(t, .(t, X2)))
delcE_in_gga(t, X1, .(f, X1)) → delcE_out_gga(t, X1, .(f, X1))
delcE_in_gga(f, X1, .(t, X2)) → U55_gga(X1, X2, delcI_in_ga(.(f, X1), X2))
U55_gga(X1, X2, delcI_out_ga(.(f, X1), X2)) → delcE_out_gga(f, X1, .(t, X2))
maxcF_in_gg([], f) → maxcF_out_gg([], f)
maxcF_in_gg(.(f, X1), X2) → U51_gg(X1, X2, maxcF_in_gg(X1, X2))
maxcF_in_gg(.(t, X1), X2) → U52_gg(X1, X2, maxcC_in_gg(X1, X2))
U52_gg(X1, X2, maxcC_out_gg(X1, X2)) → maxcF_out_gg(.(t, X1), X2)
U51_gg(X1, X2, maxcF_out_gg(X1, X2)) → maxcF_out_gg(.(f, X1), X2)
maxcF_in_ga([], f) → maxcF_out_ga([], f)
maxcF_in_ga(.(f, X1), X2) → U51_ga(X1, X2, maxcF_in_ga(X1, X2))
maxcF_in_ga(.(t, X1), X2) → U52_ga(X1, X2, maxcC_in_ga(X1, X2))
U52_ga(X1, X2, maxcC_out_ga(X1, X2)) → maxcF_out_ga(.(t, X1), X2)
U51_ga(X1, X2, maxcF_out_ga(X1, X2)) → maxcF_out_ga(.(f, X1), X2)
delcG_in_gga(f, X1, .(f, X1)) → delcG_out_gga(f, X1, .(f, X1))
delcG_in_gga(t, X1, .(f, .(f, X2))) → U56_gga(X1, X2, delcJ_in_ga(X1, X2))
delcJ_in_ga([], []) → delcJ_out_ga([], [])
delcJ_in_ga(.(t, X1), X1) → delcJ_out_ga(.(t, X1), X1)
delcJ_in_ga(.(f, X1), .(f, X2)) → U53_ga(X1, X2, delcJ_in_ga(X1, X2))
U53_ga(X1, X2, delcJ_out_ga(X1, X2)) → delcJ_out_ga(.(f, X1), .(f, X2))
U56_gga(X1, X2, delcJ_out_ga(X1, X2)) → delcG_out_gga(t, X1, .(f, .(f, X2)))
delcH_in_gga(f, X1, .(t, X1)) → delcH_out_gga(f, X1, .(t, X1))
delcH_in_gga(t, X1, .(f, X2)) → U57_gga(X1, X2, delcJ_in_ga(.(t, X1), X2))
U57_gga(X1, X2, delcJ_out_ga(.(t, X1), X2)) → delcH_out_gga(t, X1, .(f, X2))
DELJ_IN_GA(.(f, X1), .(f, X2)) → DELJ_IN_GA(X1, X2)
DELJ_IN_GA(.(f, X1)) → DELJ_IN_GA(X1)
From the DPs we obtained the following set of size-change graphs:
DELI_IN_GA(.(t, X1), .(t, X2)) → DELI_IN_GA(X1, X2)
delcB_in_ga(t, []) → delcB_out_ga(t, [])
delcB_in_ga(f, []) → delcB_out_ga(f, [])
maxcC_in_gg([], t) → maxcC_out_gg([], t)
maxcC_in_gg(.(t, X1), X2) → U48_gg(X1, X2, maxcC_in_gg(X1, X2))
maxcC_in_gg(.(f, X1), X2) → U49_gg(X1, X2, maxcC_in_gg(X1, X2))
U49_gg(X1, X2, maxcC_out_gg(X1, X2)) → maxcC_out_gg(.(f, X1), X2)
U48_gg(X1, X2, maxcC_out_gg(X1, X2)) → maxcC_out_gg(.(t, X1), X2)
maxcC_in_ga([], t) → maxcC_out_ga([], t)
maxcC_in_ga(.(t, X1), X2) → U48_ga(X1, X2, maxcC_in_ga(X1, X2))
maxcC_in_ga(.(f, X1), X2) → U49_ga(X1, X2, maxcC_in_ga(X1, X2))
U49_ga(X1, X2, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(f, X1), X2)
U48_ga(X1, X2, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(t, X1), X2)
delcD_in_gga(t, X1, .(t, X1)) → delcD_out_gga(t, X1, .(t, X1))
delcD_in_gga(f, X1, .(t, .(t, X2))) → U54_gga(X1, X2, delcI_in_ga(X1, X2))
delcI_in_ga([], []) → delcI_out_ga([], [])
delcI_in_ga(.(f, X1), X1) → delcI_out_ga(.(f, X1), X1)
delcI_in_ga(.(t, X1), .(t, X2)) → U50_ga(X1, X2, delcI_in_ga(X1, X2))
U50_ga(X1, X2, delcI_out_ga(X1, X2)) → delcI_out_ga(.(t, X1), .(t, X2))
U54_gga(X1, X2, delcI_out_ga(X1, X2)) → delcD_out_gga(f, X1, .(t, .(t, X2)))
delcE_in_gga(t, X1, .(f, X1)) → delcE_out_gga(t, X1, .(f, X1))
delcE_in_gga(f, X1, .(t, X2)) → U55_gga(X1, X2, delcI_in_ga(.(f, X1), X2))
U55_gga(X1, X2, delcI_out_ga(.(f, X1), X2)) → delcE_out_gga(f, X1, .(t, X2))
maxcF_in_gg([], f) → maxcF_out_gg([], f)
maxcF_in_gg(.(f, X1), X2) → U51_gg(X1, X2, maxcF_in_gg(X1, X2))
maxcF_in_gg(.(t, X1), X2) → U52_gg(X1, X2, maxcC_in_gg(X1, X2))
U52_gg(X1, X2, maxcC_out_gg(X1, X2)) → maxcF_out_gg(.(t, X1), X2)
U51_gg(X1, X2, maxcF_out_gg(X1, X2)) → maxcF_out_gg(.(f, X1), X2)
maxcF_in_ga([], f) → maxcF_out_ga([], f)
maxcF_in_ga(.(f, X1), X2) → U51_ga(X1, X2, maxcF_in_ga(X1, X2))
maxcF_in_ga(.(t, X1), X2) → U52_ga(X1, X2, maxcC_in_ga(X1, X2))
U52_ga(X1, X2, maxcC_out_ga(X1, X2)) → maxcF_out_ga(.(t, X1), X2)
U51_ga(X1, X2, maxcF_out_ga(X1, X2)) → maxcF_out_ga(.(f, X1), X2)
delcG_in_gga(f, X1, .(f, X1)) → delcG_out_gga(f, X1, .(f, X1))
delcG_in_gga(t, X1, .(f, .(f, X2))) → U56_gga(X1, X2, delcJ_in_ga(X1, X2))
delcJ_in_ga([], []) → delcJ_out_ga([], [])
delcJ_in_ga(.(t, X1), X1) → delcJ_out_ga(.(t, X1), X1)
delcJ_in_ga(.(f, X1), .(f, X2)) → U53_ga(X1, X2, delcJ_in_ga(X1, X2))
U53_ga(X1, X2, delcJ_out_ga(X1, X2)) → delcJ_out_ga(.(f, X1), .(f, X2))
U56_gga(X1, X2, delcJ_out_ga(X1, X2)) → delcG_out_gga(t, X1, .(f, .(f, X2)))
delcH_in_gga(f, X1, .(t, X1)) → delcH_out_gga(f, X1, .(t, X1))
delcH_in_gga(t, X1, .(f, X2)) → U57_gga(X1, X2, delcJ_in_ga(.(t, X1), X2))
U57_gga(X1, X2, delcJ_out_ga(.(t, X1), X2)) → delcH_out_gga(t, X1, .(f, X2))
DELI_IN_GA(.(t, X1), .(t, X2)) → DELI_IN_GA(X1, X2)
DELI_IN_GA(.(t, X1)) → DELI_IN_GA(X1)
From the DPs we obtained the following set of size-change graphs:
MAXC_IN_GA(.(f, X1), X2) → MAXC_IN_GA(X1, X2)
MAXC_IN_GA(.(t, X1), X2) → MAXC_IN_GA(X1, X2)
delcB_in_ga(t, []) → delcB_out_ga(t, [])
delcB_in_ga(f, []) → delcB_out_ga(f, [])
maxcC_in_gg([], t) → maxcC_out_gg([], t)
maxcC_in_gg(.(t, X1), X2) → U48_gg(X1, X2, maxcC_in_gg(X1, X2))
maxcC_in_gg(.(f, X1), X2) → U49_gg(X1, X2, maxcC_in_gg(X1, X2))
U49_gg(X1, X2, maxcC_out_gg(X1, X2)) → maxcC_out_gg(.(f, X1), X2)
U48_gg(X1, X2, maxcC_out_gg(X1, X2)) → maxcC_out_gg(.(t, X1), X2)
maxcC_in_ga([], t) → maxcC_out_ga([], t)
maxcC_in_ga(.(t, X1), X2) → U48_ga(X1, X2, maxcC_in_ga(X1, X2))
maxcC_in_ga(.(f, X1), X2) → U49_ga(X1, X2, maxcC_in_ga(X1, X2))
U49_ga(X1, X2, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(f, X1), X2)
U48_ga(X1, X2, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(t, X1), X2)
delcD_in_gga(t, X1, .(t, X1)) → delcD_out_gga(t, X1, .(t, X1))
delcD_in_gga(f, X1, .(t, .(t, X2))) → U54_gga(X1, X2, delcI_in_ga(X1, X2))
delcI_in_ga([], []) → delcI_out_ga([], [])
delcI_in_ga(.(f, X1), X1) → delcI_out_ga(.(f, X1), X1)
delcI_in_ga(.(t, X1), .(t, X2)) → U50_ga(X1, X2, delcI_in_ga(X1, X2))
U50_ga(X1, X2, delcI_out_ga(X1, X2)) → delcI_out_ga(.(t, X1), .(t, X2))
U54_gga(X1, X2, delcI_out_ga(X1, X2)) → delcD_out_gga(f, X1, .(t, .(t, X2)))
delcE_in_gga(t, X1, .(f, X1)) → delcE_out_gga(t, X1, .(f, X1))
delcE_in_gga(f, X1, .(t, X2)) → U55_gga(X1, X2, delcI_in_ga(.(f, X1), X2))
U55_gga(X1, X2, delcI_out_ga(.(f, X1), X2)) → delcE_out_gga(f, X1, .(t, X2))
maxcF_in_gg([], f) → maxcF_out_gg([], f)
maxcF_in_gg(.(f, X1), X2) → U51_gg(X1, X2, maxcF_in_gg(X1, X2))
maxcF_in_gg(.(t, X1), X2) → U52_gg(X1, X2, maxcC_in_gg(X1, X2))
U52_gg(X1, X2, maxcC_out_gg(X1, X2)) → maxcF_out_gg(.(t, X1), X2)
U51_gg(X1, X2, maxcF_out_gg(X1, X2)) → maxcF_out_gg(.(f, X1), X2)
maxcF_in_ga([], f) → maxcF_out_ga([], f)
maxcF_in_ga(.(f, X1), X2) → U51_ga(X1, X2, maxcF_in_ga(X1, X2))
maxcF_in_ga(.(t, X1), X2) → U52_ga(X1, X2, maxcC_in_ga(X1, X2))
U52_ga(X1, X2, maxcC_out_ga(X1, X2)) → maxcF_out_ga(.(t, X1), X2)
U51_ga(X1, X2, maxcF_out_ga(X1, X2)) → maxcF_out_ga(.(f, X1), X2)
delcG_in_gga(f, X1, .(f, X1)) → delcG_out_gga(f, X1, .(f, X1))
delcG_in_gga(t, X1, .(f, .(f, X2))) → U56_gga(X1, X2, delcJ_in_ga(X1, X2))
delcJ_in_ga([], []) → delcJ_out_ga([], [])
delcJ_in_ga(.(t, X1), X1) → delcJ_out_ga(.(t, X1), X1)
delcJ_in_ga(.(f, X1), .(f, X2)) → U53_ga(X1, X2, delcJ_in_ga(X1, X2))
U53_ga(X1, X2, delcJ_out_ga(X1, X2)) → delcJ_out_ga(.(f, X1), .(f, X2))
U56_gga(X1, X2, delcJ_out_ga(X1, X2)) → delcG_out_gga(t, X1, .(f, .(f, X2)))
delcH_in_gga(f, X1, .(t, X1)) → delcH_out_gga(f, X1, .(t, X1))
delcH_in_gga(t, X1, .(f, X2)) → U57_gga(X1, X2, delcJ_in_ga(.(t, X1), X2))
U57_gga(X1, X2, delcJ_out_ga(.(t, X1), X2)) → delcH_out_gga(t, X1, .(f, X2))
MAXC_IN_GA(.(f, X1), X2) → MAXC_IN_GA(X1, X2)
MAXC_IN_GA(.(t, X1), X2) → MAXC_IN_GA(X1, X2)
MAXC_IN_GA(.(f, X1)) → MAXC_IN_GA(X1)
MAXC_IN_GA(.(t, X1)) → MAXC_IN_GA(X1)
From the DPs we obtained the following set of size-change graphs:
MAXF_IN_GA(.(f, X1), X2) → MAXF_IN_GA(X1, X2)
delcB_in_ga(t, []) → delcB_out_ga(t, [])
delcB_in_ga(f, []) → delcB_out_ga(f, [])
maxcC_in_gg([], t) → maxcC_out_gg([], t)
maxcC_in_gg(.(t, X1), X2) → U48_gg(X1, X2, maxcC_in_gg(X1, X2))
maxcC_in_gg(.(f, X1), X2) → U49_gg(X1, X2, maxcC_in_gg(X1, X2))
U49_gg(X1, X2, maxcC_out_gg(X1, X2)) → maxcC_out_gg(.(f, X1), X2)
U48_gg(X1, X2, maxcC_out_gg(X1, X2)) → maxcC_out_gg(.(t, X1), X2)
maxcC_in_ga([], t) → maxcC_out_ga([], t)
maxcC_in_ga(.(t, X1), X2) → U48_ga(X1, X2, maxcC_in_ga(X1, X2))
maxcC_in_ga(.(f, X1), X2) → U49_ga(X1, X2, maxcC_in_ga(X1, X2))
U49_ga(X1, X2, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(f, X1), X2)
U48_ga(X1, X2, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(t, X1), X2)
delcD_in_gga(t, X1, .(t, X1)) → delcD_out_gga(t, X1, .(t, X1))
delcD_in_gga(f, X1, .(t, .(t, X2))) → U54_gga(X1, X2, delcI_in_ga(X1, X2))
delcI_in_ga([], []) → delcI_out_ga([], [])
delcI_in_ga(.(f, X1), X1) → delcI_out_ga(.(f, X1), X1)
delcI_in_ga(.(t, X1), .(t, X2)) → U50_ga(X1, X2, delcI_in_ga(X1, X2))
U50_ga(X1, X2, delcI_out_ga(X1, X2)) → delcI_out_ga(.(t, X1), .(t, X2))
U54_gga(X1, X2, delcI_out_ga(X1, X2)) → delcD_out_gga(f, X1, .(t, .(t, X2)))
delcE_in_gga(t, X1, .(f, X1)) → delcE_out_gga(t, X1, .(f, X1))
delcE_in_gga(f, X1, .(t, X2)) → U55_gga(X1, X2, delcI_in_ga(.(f, X1), X2))
U55_gga(X1, X2, delcI_out_ga(.(f, X1), X2)) → delcE_out_gga(f, X1, .(t, X2))
maxcF_in_gg([], f) → maxcF_out_gg([], f)
maxcF_in_gg(.(f, X1), X2) → U51_gg(X1, X2, maxcF_in_gg(X1, X2))
maxcF_in_gg(.(t, X1), X2) → U52_gg(X1, X2, maxcC_in_gg(X1, X2))
U52_gg(X1, X2, maxcC_out_gg(X1, X2)) → maxcF_out_gg(.(t, X1), X2)
U51_gg(X1, X2, maxcF_out_gg(X1, X2)) → maxcF_out_gg(.(f, X1), X2)
maxcF_in_ga([], f) → maxcF_out_ga([], f)
maxcF_in_ga(.(f, X1), X2) → U51_ga(X1, X2, maxcF_in_ga(X1, X2))
maxcF_in_ga(.(t, X1), X2) → U52_ga(X1, X2, maxcC_in_ga(X1, X2))
U52_ga(X1, X2, maxcC_out_ga(X1, X2)) → maxcF_out_ga(.(t, X1), X2)
U51_ga(X1, X2, maxcF_out_ga(X1, X2)) → maxcF_out_ga(.(f, X1), X2)
delcG_in_gga(f, X1, .(f, X1)) → delcG_out_gga(f, X1, .(f, X1))
delcG_in_gga(t, X1, .(f, .(f, X2))) → U56_gga(X1, X2, delcJ_in_ga(X1, X2))
delcJ_in_ga([], []) → delcJ_out_ga([], [])
delcJ_in_ga(.(t, X1), X1) → delcJ_out_ga(.(t, X1), X1)
delcJ_in_ga(.(f, X1), .(f, X2)) → U53_ga(X1, X2, delcJ_in_ga(X1, X2))
U53_ga(X1, X2, delcJ_out_ga(X1, X2)) → delcJ_out_ga(.(f, X1), .(f, X2))
U56_gga(X1, X2, delcJ_out_ga(X1, X2)) → delcG_out_gga(t, X1, .(f, .(f, X2)))
delcH_in_gga(f, X1, .(t, X1)) → delcH_out_gga(f, X1, .(t, X1))
delcH_in_gga(t, X1, .(f, X2)) → U57_gga(X1, X2, delcJ_in_ga(.(t, X1), X2))
U57_gga(X1, X2, delcJ_out_ga(.(t, X1), X2)) → delcH_out_gga(t, X1, .(f, X2))
MAXF_IN_GA(.(f, X1), X2) → MAXF_IN_GA(X1, X2)
MAXF_IN_GA(.(f, X1)) → MAXF_IN_GA(X1)
From the DPs we obtained the following set of size-change graphs:
U7_GA(X1, X2, delcB_out_ga(X1, X3)) → MAXSORTA_IN_GA(X3, X2)
MAXSORTA_IN_GA(.(X1, []), .(X1, X2)) → U7_GA(X1, X2, delcB_in_ga(X1, X3))
MAXSORTA_IN_GA(.(t, .(t, X1)), .(X2, X3)) → U12_GA(X1, X2, X3, maxcC_in_ga(X1, X2))
U12_GA(X1, X2, X3, maxcC_out_ga(X1, X2)) → U13_GA(X1, X2, X3, delcD_in_gga(X2, X1, X4))
U13_GA(X1, X2, X3, delcD_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4, X3)
MAXSORTA_IN_GA(.(t, .(f, X1)), .(X2, X3)) → U18_GA(X1, X2, X3, maxcC_in_ga(X1, X2))
U18_GA(X1, X2, X3, maxcC_out_ga(X1, X2)) → U19_GA(X1, X2, X3, delcE_in_gga(X2, X1, X4))
U19_GA(X1, X2, X3, delcE_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4, X3)
MAXSORTA_IN_GA(.(f, .(f, X1)), .(X2, X3)) → U24_GA(X1, X2, X3, maxcF_in_ga(X1, X2))
U24_GA(X1, X2, X3, maxcF_out_ga(X1, X2)) → U25_GA(X1, X2, X3, delcG_in_gga(X2, X1, X4))
U25_GA(X1, X2, X3, delcG_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4, X3)
MAXSORTA_IN_GA(.(f, .(t, X1)), .(X2, X3)) → U30_GA(X1, X2, X3, maxcC_in_ga(X1, X2))
U30_GA(X1, X2, X3, maxcC_out_ga(X1, X2)) → U31_GA(X1, X2, X3, delcH_in_gga(X2, X1, X4))
U31_GA(X1, X2, X3, delcH_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4, X3)
delcB_in_ga(t, []) → delcB_out_ga(t, [])
delcB_in_ga(f, []) → delcB_out_ga(f, [])
maxcC_in_gg([], t) → maxcC_out_gg([], t)
maxcC_in_gg(.(t, X1), X2) → U48_gg(X1, X2, maxcC_in_gg(X1, X2))
maxcC_in_gg(.(f, X1), X2) → U49_gg(X1, X2, maxcC_in_gg(X1, X2))
U49_gg(X1, X2, maxcC_out_gg(X1, X2)) → maxcC_out_gg(.(f, X1), X2)
U48_gg(X1, X2, maxcC_out_gg(X1, X2)) → maxcC_out_gg(.(t, X1), X2)
maxcC_in_ga([], t) → maxcC_out_ga([], t)
maxcC_in_ga(.(t, X1), X2) → U48_ga(X1, X2, maxcC_in_ga(X1, X2))
maxcC_in_ga(.(f, X1), X2) → U49_ga(X1, X2, maxcC_in_ga(X1, X2))
U49_ga(X1, X2, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(f, X1), X2)
U48_ga(X1, X2, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(t, X1), X2)
delcD_in_gga(t, X1, .(t, X1)) → delcD_out_gga(t, X1, .(t, X1))
delcD_in_gga(f, X1, .(t, .(t, X2))) → U54_gga(X1, X2, delcI_in_ga(X1, X2))
delcI_in_ga([], []) → delcI_out_ga([], [])
delcI_in_ga(.(f, X1), X1) → delcI_out_ga(.(f, X1), X1)
delcI_in_ga(.(t, X1), .(t, X2)) → U50_ga(X1, X2, delcI_in_ga(X1, X2))
U50_ga(X1, X2, delcI_out_ga(X1, X2)) → delcI_out_ga(.(t, X1), .(t, X2))
U54_gga(X1, X2, delcI_out_ga(X1, X2)) → delcD_out_gga(f, X1, .(t, .(t, X2)))
delcE_in_gga(t, X1, .(f, X1)) → delcE_out_gga(t, X1, .(f, X1))
delcE_in_gga(f, X1, .(t, X2)) → U55_gga(X1, X2, delcI_in_ga(.(f, X1), X2))
U55_gga(X1, X2, delcI_out_ga(.(f, X1), X2)) → delcE_out_gga(f, X1, .(t, X2))
maxcF_in_gg([], f) → maxcF_out_gg([], f)
maxcF_in_gg(.(f, X1), X2) → U51_gg(X1, X2, maxcF_in_gg(X1, X2))
maxcF_in_gg(.(t, X1), X2) → U52_gg(X1, X2, maxcC_in_gg(X1, X2))
U52_gg(X1, X2, maxcC_out_gg(X1, X2)) → maxcF_out_gg(.(t, X1), X2)
U51_gg(X1, X2, maxcF_out_gg(X1, X2)) → maxcF_out_gg(.(f, X1), X2)
maxcF_in_ga([], f) → maxcF_out_ga([], f)
maxcF_in_ga(.(f, X1), X2) → U51_ga(X1, X2, maxcF_in_ga(X1, X2))
maxcF_in_ga(.(t, X1), X2) → U52_ga(X1, X2, maxcC_in_ga(X1, X2))
U52_ga(X1, X2, maxcC_out_ga(X1, X2)) → maxcF_out_ga(.(t, X1), X2)
U51_ga(X1, X2, maxcF_out_ga(X1, X2)) → maxcF_out_ga(.(f, X1), X2)
delcG_in_gga(f, X1, .(f, X1)) → delcG_out_gga(f, X1, .(f, X1))
delcG_in_gga(t, X1, .(f, .(f, X2))) → U56_gga(X1, X2, delcJ_in_ga(X1, X2))
delcJ_in_ga([], []) → delcJ_out_ga([], [])
delcJ_in_ga(.(t, X1), X1) → delcJ_out_ga(.(t, X1), X1)
delcJ_in_ga(.(f, X1), .(f, X2)) → U53_ga(X1, X2, delcJ_in_ga(X1, X2))
U53_ga(X1, X2, delcJ_out_ga(X1, X2)) → delcJ_out_ga(.(f, X1), .(f, X2))
U56_gga(X1, X2, delcJ_out_ga(X1, X2)) → delcG_out_gga(t, X1, .(f, .(f, X2)))
delcH_in_gga(f, X1, .(t, X1)) → delcH_out_gga(f, X1, .(t, X1))
delcH_in_gga(t, X1, .(f, X2)) → U57_gga(X1, X2, delcJ_in_ga(.(t, X1), X2))
U57_gga(X1, X2, delcJ_out_ga(.(t, X1), X2)) → delcH_out_gga(t, X1, .(f, X2))
U7_GA(X1, X2, delcB_out_ga(X1, X3)) → MAXSORTA_IN_GA(X3, X2)
MAXSORTA_IN_GA(.(X1, []), .(X1, X2)) → U7_GA(X1, X2, delcB_in_ga(X1, X3))
MAXSORTA_IN_GA(.(t, .(t, X1)), .(X2, X3)) → U12_GA(X1, X2, X3, maxcC_in_ga(X1, X2))
U12_GA(X1, X2, X3, maxcC_out_ga(X1, X2)) → U13_GA(X1, X2, X3, delcD_in_gga(X2, X1, X4))
U13_GA(X1, X2, X3, delcD_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4, X3)
MAXSORTA_IN_GA(.(t, .(f, X1)), .(X2, X3)) → U18_GA(X1, X2, X3, maxcC_in_ga(X1, X2))
U18_GA(X1, X2, X3, maxcC_out_ga(X1, X2)) → U19_GA(X1, X2, X3, delcE_in_gga(X2, X1, X4))
U19_GA(X1, X2, X3, delcE_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4, X3)
MAXSORTA_IN_GA(.(f, .(f, X1)), .(X2, X3)) → U24_GA(X1, X2, X3, maxcF_in_ga(X1, X2))
U24_GA(X1, X2, X3, maxcF_out_ga(X1, X2)) → U25_GA(X1, X2, X3, delcG_in_gga(X2, X1, X4))
U25_GA(X1, X2, X3, delcG_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4, X3)
MAXSORTA_IN_GA(.(f, .(t, X1)), .(X2, X3)) → U30_GA(X1, X2, X3, maxcC_in_ga(X1, X2))
U30_GA(X1, X2, X3, maxcC_out_ga(X1, X2)) → U31_GA(X1, X2, X3, delcH_in_gga(X2, X1, X4))
U31_GA(X1, X2, X3, delcH_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4, X3)
delcB_in_ga(t, []) → delcB_out_ga(t, [])
delcB_in_ga(f, []) → delcB_out_ga(f, [])
maxcC_in_ga([], t) → maxcC_out_ga([], t)
maxcC_in_ga(.(t, X1), X2) → U48_ga(X1, X2, maxcC_in_ga(X1, X2))
maxcC_in_ga(.(f, X1), X2) → U49_ga(X1, X2, maxcC_in_ga(X1, X2))
delcD_in_gga(t, X1, .(t, X1)) → delcD_out_gga(t, X1, .(t, X1))
delcD_in_gga(f, X1, .(t, .(t, X2))) → U54_gga(X1, X2, delcI_in_ga(X1, X2))
delcE_in_gga(t, X1, .(f, X1)) → delcE_out_gga(t, X1, .(f, X1))
delcE_in_gga(f, X1, .(t, X2)) → U55_gga(X1, X2, delcI_in_ga(.(f, X1), X2))
maxcF_in_ga([], f) → maxcF_out_ga([], f)
maxcF_in_ga(.(f, X1), X2) → U51_ga(X1, X2, maxcF_in_ga(X1, X2))
maxcF_in_ga(.(t, X1), X2) → U52_ga(X1, X2, maxcC_in_ga(X1, X2))
delcG_in_gga(f, X1, .(f, X1)) → delcG_out_gga(f, X1, .(f, X1))
delcG_in_gga(t, X1, .(f, .(f, X2))) → U56_gga(X1, X2, delcJ_in_ga(X1, X2))
delcH_in_gga(f, X1, .(t, X1)) → delcH_out_gga(f, X1, .(t, X1))
delcH_in_gga(t, X1, .(f, X2)) → U57_gga(X1, X2, delcJ_in_ga(.(t, X1), X2))
U48_ga(X1, X2, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(t, X1), X2)
U49_ga(X1, X2, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(f, X1), X2)
U54_gga(X1, X2, delcI_out_ga(X1, X2)) → delcD_out_gga(f, X1, .(t, .(t, X2)))
U55_gga(X1, X2, delcI_out_ga(.(f, X1), X2)) → delcE_out_gga(f, X1, .(t, X2))
U51_ga(X1, X2, maxcF_out_ga(X1, X2)) → maxcF_out_ga(.(f, X1), X2)
U52_ga(X1, X2, maxcC_out_ga(X1, X2)) → maxcF_out_ga(.(t, X1), X2)
U56_gga(X1, X2, delcJ_out_ga(X1, X2)) → delcG_out_gga(t, X1, .(f, .(f, X2)))
U57_gga(X1, X2, delcJ_out_ga(.(t, X1), X2)) → delcH_out_gga(t, X1, .(f, X2))
delcI_in_ga([], []) → delcI_out_ga([], [])
delcI_in_ga(.(f, X1), X1) → delcI_out_ga(.(f, X1), X1)
delcI_in_ga(.(t, X1), .(t, X2)) → U50_ga(X1, X2, delcI_in_ga(X1, X2))
delcJ_in_ga([], []) → delcJ_out_ga([], [])
delcJ_in_ga(.(t, X1), X1) → delcJ_out_ga(.(t, X1), X1)
delcJ_in_ga(.(f, X1), .(f, X2)) → U53_ga(X1, X2, delcJ_in_ga(X1, X2))
U50_ga(X1, X2, delcI_out_ga(X1, X2)) → delcI_out_ga(.(t, X1), .(t, X2))
U53_ga(X1, X2, delcJ_out_ga(X1, X2)) → delcJ_out_ga(.(f, X1), .(f, X2))
U7_GA(X1, delcB_out_ga(X1, X3)) → MAXSORTA_IN_GA(X3)
MAXSORTA_IN_GA(.(X1, [])) → U7_GA(X1, delcB_in_ga(X1))
MAXSORTA_IN_GA(.(t, .(t, X1))) → U12_GA(X1, maxcC_in_ga(X1))
U12_GA(X1, maxcC_out_ga(X1, X2)) → U13_GA(X1, delcD_in_gga(X2, X1))
U13_GA(X1, delcD_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(t, .(f, X1))) → U18_GA(X1, maxcC_in_ga(X1))
U18_GA(X1, maxcC_out_ga(X1, X2)) → U19_GA(X1, delcE_in_gga(X2, X1))
U19_GA(X1, delcE_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(f, .(f, X1))) → U24_GA(X1, maxcF_in_ga(X1))
U24_GA(X1, maxcF_out_ga(X1, X2)) → U25_GA(X1, delcG_in_gga(X2, X1))
U25_GA(X1, delcG_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(f, .(t, X1))) → U30_GA(X1, maxcC_in_ga(X1))
U30_GA(X1, maxcC_out_ga(X1, X2)) → U31_GA(X1, delcH_in_gga(X2, X1))
U31_GA(X1, delcH_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
delcB_in_ga(t) → delcB_out_ga(t, [])
delcB_in_ga(f) → delcB_out_ga(f, [])
maxcC_in_ga([]) → maxcC_out_ga([], t)
maxcC_in_ga(.(t, X1)) → U48_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga(.(f, X1)) → U49_ga(X1, maxcC_in_ga(X1))
delcD_in_gga(t, X1) → delcD_out_gga(t, X1, .(t, X1))
delcD_in_gga(f, X1) → U54_gga(X1, delcI_in_ga(X1))
delcE_in_gga(t, X1) → delcE_out_gga(t, X1, .(f, X1))
delcE_in_gga(f, X1) → U55_gga(X1, delcI_in_ga(.(f, X1)))
maxcF_in_ga([]) → maxcF_out_ga([], f)
maxcF_in_ga(.(f, X1)) → U51_ga(X1, maxcF_in_ga(X1))
maxcF_in_ga(.(t, X1)) → U52_ga(X1, maxcC_in_ga(X1))
delcG_in_gga(f, X1) → delcG_out_gga(f, X1, .(f, X1))
delcG_in_gga(t, X1) → U56_gga(X1, delcJ_in_ga(X1))
delcH_in_gga(f, X1) → delcH_out_gga(f, X1, .(t, X1))
delcH_in_gga(t, X1) → U57_gga(X1, delcJ_in_ga(.(t, X1)))
U48_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(t, X1), X2)
U49_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(f, X1), X2)
U54_gga(X1, delcI_out_ga(X1, X2)) → delcD_out_gga(f, X1, .(t, .(t, X2)))
U55_gga(X1, delcI_out_ga(.(f, X1), X2)) → delcE_out_gga(f, X1, .(t, X2))
U51_ga(X1, maxcF_out_ga(X1, X2)) → maxcF_out_ga(.(f, X1), X2)
U52_ga(X1, maxcC_out_ga(X1, X2)) → maxcF_out_ga(.(t, X1), X2)
U56_gga(X1, delcJ_out_ga(X1, X2)) → delcG_out_gga(t, X1, .(f, .(f, X2)))
U57_gga(X1, delcJ_out_ga(.(t, X1), X2)) → delcH_out_gga(t, X1, .(f, X2))
delcI_in_ga([]) → delcI_out_ga([], [])
delcI_in_ga(.(f, X1)) → delcI_out_ga(.(f, X1), X1)
delcI_in_ga(.(t, X1)) → U50_ga(X1, delcI_in_ga(X1))
delcJ_in_ga([]) → delcJ_out_ga([], [])
delcJ_in_ga(.(t, X1)) → delcJ_out_ga(.(t, X1), X1)
delcJ_in_ga(.(f, X1)) → U53_ga(X1, delcJ_in_ga(X1))
U50_ga(X1, delcI_out_ga(X1, X2)) → delcI_out_ga(.(t, X1), .(t, X2))
U53_ga(X1, delcJ_out_ga(X1, X2)) → delcJ_out_ga(.(f, X1), .(f, X2))
delcB_in_ga(x0)
maxcC_in_ga(x0)
delcD_in_gga(x0, x1)
delcE_in_gga(x0, x1)
maxcF_in_ga(x0)
delcG_in_gga(x0, x1)
delcH_in_gga(x0, x1)
U48_ga(x0, x1)
U49_ga(x0, x1)
U54_gga(x0, x1)
U55_gga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)
U56_gga(x0, x1)
U57_gga(x0, x1)
delcI_in_ga(x0)
delcJ_in_ga(x0)
U50_ga(x0, x1)
U53_ga(x0, x1)
MAXSORTA_IN_GA(.(t, [])) → U7_GA(t, delcB_out_ga(t, []))
MAXSORTA_IN_GA(.(f, [])) → U7_GA(f, delcB_out_ga(f, []))
U7_GA(X1, delcB_out_ga(X1, X3)) → MAXSORTA_IN_GA(X3)
MAXSORTA_IN_GA(.(t, .(t, X1))) → U12_GA(X1, maxcC_in_ga(X1))
U12_GA(X1, maxcC_out_ga(X1, X2)) → U13_GA(X1, delcD_in_gga(X2, X1))
U13_GA(X1, delcD_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(t, .(f, X1))) → U18_GA(X1, maxcC_in_ga(X1))
U18_GA(X1, maxcC_out_ga(X1, X2)) → U19_GA(X1, delcE_in_gga(X2, X1))
U19_GA(X1, delcE_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(f, .(f, X1))) → U24_GA(X1, maxcF_in_ga(X1))
U24_GA(X1, maxcF_out_ga(X1, X2)) → U25_GA(X1, delcG_in_gga(X2, X1))
U25_GA(X1, delcG_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(f, .(t, X1))) → U30_GA(X1, maxcC_in_ga(X1))
U30_GA(X1, maxcC_out_ga(X1, X2)) → U31_GA(X1, delcH_in_gga(X2, X1))
U31_GA(X1, delcH_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(t, [])) → U7_GA(t, delcB_out_ga(t, []))
MAXSORTA_IN_GA(.(f, [])) → U7_GA(f, delcB_out_ga(f, []))
delcB_in_ga(t) → delcB_out_ga(t, [])
delcB_in_ga(f) → delcB_out_ga(f, [])
maxcC_in_ga([]) → maxcC_out_ga([], t)
maxcC_in_ga(.(t, X1)) → U48_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga(.(f, X1)) → U49_ga(X1, maxcC_in_ga(X1))
delcD_in_gga(t, X1) → delcD_out_gga(t, X1, .(t, X1))
delcD_in_gga(f, X1) → U54_gga(X1, delcI_in_ga(X1))
delcE_in_gga(t, X1) → delcE_out_gga(t, X1, .(f, X1))
delcE_in_gga(f, X1) → U55_gga(X1, delcI_in_ga(.(f, X1)))
maxcF_in_ga([]) → maxcF_out_ga([], f)
maxcF_in_ga(.(f, X1)) → U51_ga(X1, maxcF_in_ga(X1))
maxcF_in_ga(.(t, X1)) → U52_ga(X1, maxcC_in_ga(X1))
delcG_in_gga(f, X1) → delcG_out_gga(f, X1, .(f, X1))
delcG_in_gga(t, X1) → U56_gga(X1, delcJ_in_ga(X1))
delcH_in_gga(f, X1) → delcH_out_gga(f, X1, .(t, X1))
delcH_in_gga(t, X1) → U57_gga(X1, delcJ_in_ga(.(t, X1)))
U48_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(t, X1), X2)
U49_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(f, X1), X2)
U54_gga(X1, delcI_out_ga(X1, X2)) → delcD_out_gga(f, X1, .(t, .(t, X2)))
U55_gga(X1, delcI_out_ga(.(f, X1), X2)) → delcE_out_gga(f, X1, .(t, X2))
U51_ga(X1, maxcF_out_ga(X1, X2)) → maxcF_out_ga(.(f, X1), X2)
U52_ga(X1, maxcC_out_ga(X1, X2)) → maxcF_out_ga(.(t, X1), X2)
U56_gga(X1, delcJ_out_ga(X1, X2)) → delcG_out_gga(t, X1, .(f, .(f, X2)))
U57_gga(X1, delcJ_out_ga(.(t, X1), X2)) → delcH_out_gga(t, X1, .(f, X2))
delcI_in_ga([]) → delcI_out_ga([], [])
delcI_in_ga(.(f, X1)) → delcI_out_ga(.(f, X1), X1)
delcI_in_ga(.(t, X1)) → U50_ga(X1, delcI_in_ga(X1))
delcJ_in_ga([]) → delcJ_out_ga([], [])
delcJ_in_ga(.(t, X1)) → delcJ_out_ga(.(t, X1), X1)
delcJ_in_ga(.(f, X1)) → U53_ga(X1, delcJ_in_ga(X1))
U50_ga(X1, delcI_out_ga(X1, X2)) → delcI_out_ga(.(t, X1), .(t, X2))
U53_ga(X1, delcJ_out_ga(X1, X2)) → delcJ_out_ga(.(f, X1), .(f, X2))
delcB_in_ga(x0)
maxcC_in_ga(x0)
delcD_in_gga(x0, x1)
delcE_in_gga(x0, x1)
maxcF_in_ga(x0)
delcG_in_gga(x0, x1)
delcH_in_gga(x0, x1)
U48_ga(x0, x1)
U49_ga(x0, x1)
U54_gga(x0, x1)
U55_gga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)
U56_gga(x0, x1)
U57_gga(x0, x1)
delcI_in_ga(x0)
delcJ_in_ga(x0)
U50_ga(x0, x1)
U53_ga(x0, x1)
U7_GA(X1, delcB_out_ga(X1, X3)) → MAXSORTA_IN_GA(X3)
MAXSORTA_IN_GA(.(t, .(t, X1))) → U12_GA(X1, maxcC_in_ga(X1))
U12_GA(X1, maxcC_out_ga(X1, X2)) → U13_GA(X1, delcD_in_gga(X2, X1))
U13_GA(X1, delcD_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(t, .(f, X1))) → U18_GA(X1, maxcC_in_ga(X1))
U18_GA(X1, maxcC_out_ga(X1, X2)) → U19_GA(X1, delcE_in_gga(X2, X1))
U19_GA(X1, delcE_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(f, .(f, X1))) → U24_GA(X1, maxcF_in_ga(X1))
U24_GA(X1, maxcF_out_ga(X1, X2)) → U25_GA(X1, delcG_in_gga(X2, X1))
U25_GA(X1, delcG_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(f, .(t, X1))) → U30_GA(X1, maxcC_in_ga(X1))
U30_GA(X1, maxcC_out_ga(X1, X2)) → U31_GA(X1, delcH_in_gga(X2, X1))
U31_GA(X1, delcH_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(t, [])) → U7_GA(t, delcB_out_ga(t, []))
MAXSORTA_IN_GA(.(f, [])) → U7_GA(f, delcB_out_ga(f, []))
delcH_in_gga(f, X1) → delcH_out_gga(f, X1, .(t, X1))
delcH_in_gga(t, X1) → U57_gga(X1, delcJ_in_ga(.(t, X1)))
delcJ_in_ga(.(t, X1)) → delcJ_out_ga(.(t, X1), X1)
U57_gga(X1, delcJ_out_ga(.(t, X1), X2)) → delcH_out_gga(t, X1, .(f, X2))
maxcC_in_ga([]) → maxcC_out_ga([], t)
maxcC_in_ga(.(t, X1)) → U48_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga(.(f, X1)) → U49_ga(X1, maxcC_in_ga(X1))
U49_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(f, X1), X2)
U48_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(t, X1), X2)
delcG_in_gga(f, X1) → delcG_out_gga(f, X1, .(f, X1))
delcG_in_gga(t, X1) → U56_gga(X1, delcJ_in_ga(X1))
delcJ_in_ga([]) → delcJ_out_ga([], [])
delcJ_in_ga(.(f, X1)) → U53_ga(X1, delcJ_in_ga(X1))
U56_gga(X1, delcJ_out_ga(X1, X2)) → delcG_out_gga(t, X1, .(f, .(f, X2)))
U53_ga(X1, delcJ_out_ga(X1, X2)) → delcJ_out_ga(.(f, X1), .(f, X2))
maxcF_in_ga([]) → maxcF_out_ga([], f)
maxcF_in_ga(.(f, X1)) → U51_ga(X1, maxcF_in_ga(X1))
maxcF_in_ga(.(t, X1)) → U52_ga(X1, maxcC_in_ga(X1))
U52_ga(X1, maxcC_out_ga(X1, X2)) → maxcF_out_ga(.(t, X1), X2)
U51_ga(X1, maxcF_out_ga(X1, X2)) → maxcF_out_ga(.(f, X1), X2)
delcE_in_gga(t, X1) → delcE_out_gga(t, X1, .(f, X1))
delcE_in_gga(f, X1) → U55_gga(X1, delcI_in_ga(.(f, X1)))
delcI_in_ga(.(f, X1)) → delcI_out_ga(.(f, X1), X1)
U55_gga(X1, delcI_out_ga(.(f, X1), X2)) → delcE_out_gga(f, X1, .(t, X2))
delcD_in_gga(t, X1) → delcD_out_gga(t, X1, .(t, X1))
delcD_in_gga(f, X1) → U54_gga(X1, delcI_in_ga(X1))
delcI_in_ga([]) → delcI_out_ga([], [])
delcI_in_ga(.(t, X1)) → U50_ga(X1, delcI_in_ga(X1))
U54_gga(X1, delcI_out_ga(X1, X2)) → delcD_out_gga(f, X1, .(t, .(t, X2)))
U50_ga(X1, delcI_out_ga(X1, X2)) → delcI_out_ga(.(t, X1), .(t, X2))
delcB_in_ga(x0)
maxcC_in_ga(x0)
delcD_in_gga(x0, x1)
delcE_in_gga(x0, x1)
maxcF_in_ga(x0)
delcG_in_gga(x0, x1)
delcH_in_gga(x0, x1)
U48_ga(x0, x1)
U49_ga(x0, x1)
U54_gga(x0, x1)
U55_gga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)
U56_gga(x0, x1)
U57_gga(x0, x1)
delcI_in_ga(x0)
delcJ_in_ga(x0)
U50_ga(x0, x1)
U53_ga(x0, x1)
delcB_in_ga(x0)
U7_GA(X1, delcB_out_ga(X1, X3)) → MAXSORTA_IN_GA(X3)
MAXSORTA_IN_GA(.(t, .(t, X1))) → U12_GA(X1, maxcC_in_ga(X1))
U12_GA(X1, maxcC_out_ga(X1, X2)) → U13_GA(X1, delcD_in_gga(X2, X1))
U13_GA(X1, delcD_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(t, .(f, X1))) → U18_GA(X1, maxcC_in_ga(X1))
U18_GA(X1, maxcC_out_ga(X1, X2)) → U19_GA(X1, delcE_in_gga(X2, X1))
U19_GA(X1, delcE_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(f, .(f, X1))) → U24_GA(X1, maxcF_in_ga(X1))
U24_GA(X1, maxcF_out_ga(X1, X2)) → U25_GA(X1, delcG_in_gga(X2, X1))
U25_GA(X1, delcG_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(f, .(t, X1))) → U30_GA(X1, maxcC_in_ga(X1))
U30_GA(X1, maxcC_out_ga(X1, X2)) → U31_GA(X1, delcH_in_gga(X2, X1))
U31_GA(X1, delcH_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(t, [])) → U7_GA(t, delcB_out_ga(t, []))
MAXSORTA_IN_GA(.(f, [])) → U7_GA(f, delcB_out_ga(f, []))
delcH_in_gga(f, X1) → delcH_out_gga(f, X1, .(t, X1))
delcH_in_gga(t, X1) → U57_gga(X1, delcJ_in_ga(.(t, X1)))
delcJ_in_ga(.(t, X1)) → delcJ_out_ga(.(t, X1), X1)
U57_gga(X1, delcJ_out_ga(.(t, X1), X2)) → delcH_out_gga(t, X1, .(f, X2))
maxcC_in_ga([]) → maxcC_out_ga([], t)
maxcC_in_ga(.(t, X1)) → U48_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga(.(f, X1)) → U49_ga(X1, maxcC_in_ga(X1))
U49_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(f, X1), X2)
U48_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(t, X1), X2)
delcG_in_gga(f, X1) → delcG_out_gga(f, X1, .(f, X1))
delcG_in_gga(t, X1) → U56_gga(X1, delcJ_in_ga(X1))
delcJ_in_ga([]) → delcJ_out_ga([], [])
delcJ_in_ga(.(f, X1)) → U53_ga(X1, delcJ_in_ga(X1))
U56_gga(X1, delcJ_out_ga(X1, X2)) → delcG_out_gga(t, X1, .(f, .(f, X2)))
U53_ga(X1, delcJ_out_ga(X1, X2)) → delcJ_out_ga(.(f, X1), .(f, X2))
maxcF_in_ga([]) → maxcF_out_ga([], f)
maxcF_in_ga(.(f, X1)) → U51_ga(X1, maxcF_in_ga(X1))
maxcF_in_ga(.(t, X1)) → U52_ga(X1, maxcC_in_ga(X1))
U52_ga(X1, maxcC_out_ga(X1, X2)) → maxcF_out_ga(.(t, X1), X2)
U51_ga(X1, maxcF_out_ga(X1, X2)) → maxcF_out_ga(.(f, X1), X2)
delcE_in_gga(t, X1) → delcE_out_gga(t, X1, .(f, X1))
delcE_in_gga(f, X1) → U55_gga(X1, delcI_in_ga(.(f, X1)))
delcI_in_ga(.(f, X1)) → delcI_out_ga(.(f, X1), X1)
U55_gga(X1, delcI_out_ga(.(f, X1), X2)) → delcE_out_gga(f, X1, .(t, X2))
delcD_in_gga(t, X1) → delcD_out_gga(t, X1, .(t, X1))
delcD_in_gga(f, X1) → U54_gga(X1, delcI_in_ga(X1))
delcI_in_ga([]) → delcI_out_ga([], [])
delcI_in_ga(.(t, X1)) → U50_ga(X1, delcI_in_ga(X1))
U54_gga(X1, delcI_out_ga(X1, X2)) → delcD_out_gga(f, X1, .(t, .(t, X2)))
U50_ga(X1, delcI_out_ga(X1, X2)) → delcI_out_ga(.(t, X1), .(t, X2))
maxcC_in_ga(x0)
delcD_in_gga(x0, x1)
delcE_in_gga(x0, x1)
maxcF_in_ga(x0)
delcG_in_gga(x0, x1)
delcH_in_gga(x0, x1)
U48_ga(x0, x1)
U49_ga(x0, x1)
U54_gga(x0, x1)
U55_gga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)
U56_gga(x0, x1)
U57_gga(x0, x1)
delcI_in_ga(x0)
delcJ_in_ga(x0)
U50_ga(x0, x1)
U53_ga(x0, x1)
U7_GA(t, delcB_out_ga(t, [])) → MAXSORTA_IN_GA([])
U7_GA(f, delcB_out_ga(f, [])) → MAXSORTA_IN_GA([])
MAXSORTA_IN_GA(.(t, .(t, X1))) → U12_GA(X1, maxcC_in_ga(X1))
U12_GA(X1, maxcC_out_ga(X1, X2)) → U13_GA(X1, delcD_in_gga(X2, X1))
U13_GA(X1, delcD_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(t, .(f, X1))) → U18_GA(X1, maxcC_in_ga(X1))
U18_GA(X1, maxcC_out_ga(X1, X2)) → U19_GA(X1, delcE_in_gga(X2, X1))
U19_GA(X1, delcE_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(f, .(f, X1))) → U24_GA(X1, maxcF_in_ga(X1))
U24_GA(X1, maxcF_out_ga(X1, X2)) → U25_GA(X1, delcG_in_gga(X2, X1))
U25_GA(X1, delcG_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(f, .(t, X1))) → U30_GA(X1, maxcC_in_ga(X1))
U30_GA(X1, maxcC_out_ga(X1, X2)) → U31_GA(X1, delcH_in_gga(X2, X1))
U31_GA(X1, delcH_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(t, [])) → U7_GA(t, delcB_out_ga(t, []))
MAXSORTA_IN_GA(.(f, [])) → U7_GA(f, delcB_out_ga(f, []))
U7_GA(t, delcB_out_ga(t, [])) → MAXSORTA_IN_GA([])
U7_GA(f, delcB_out_ga(f, [])) → MAXSORTA_IN_GA([])
delcH_in_gga(f, X1) → delcH_out_gga(f, X1, .(t, X1))
delcH_in_gga(t, X1) → U57_gga(X1, delcJ_in_ga(.(t, X1)))
delcJ_in_ga(.(t, X1)) → delcJ_out_ga(.(t, X1), X1)
U57_gga(X1, delcJ_out_ga(.(t, X1), X2)) → delcH_out_gga(t, X1, .(f, X2))
maxcC_in_ga([]) → maxcC_out_ga([], t)
maxcC_in_ga(.(t, X1)) → U48_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga(.(f, X1)) → U49_ga(X1, maxcC_in_ga(X1))
U49_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(f, X1), X2)
U48_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(t, X1), X2)
delcG_in_gga(f, X1) → delcG_out_gga(f, X1, .(f, X1))
delcG_in_gga(t, X1) → U56_gga(X1, delcJ_in_ga(X1))
delcJ_in_ga([]) → delcJ_out_ga([], [])
delcJ_in_ga(.(f, X1)) → U53_ga(X1, delcJ_in_ga(X1))
U56_gga(X1, delcJ_out_ga(X1, X2)) → delcG_out_gga(t, X1, .(f, .(f, X2)))
U53_ga(X1, delcJ_out_ga(X1, X2)) → delcJ_out_ga(.(f, X1), .(f, X2))
maxcF_in_ga([]) → maxcF_out_ga([], f)
maxcF_in_ga(.(f, X1)) → U51_ga(X1, maxcF_in_ga(X1))
maxcF_in_ga(.(t, X1)) → U52_ga(X1, maxcC_in_ga(X1))
U52_ga(X1, maxcC_out_ga(X1, X2)) → maxcF_out_ga(.(t, X1), X2)
U51_ga(X1, maxcF_out_ga(X1, X2)) → maxcF_out_ga(.(f, X1), X2)
delcE_in_gga(t, X1) → delcE_out_gga(t, X1, .(f, X1))
delcE_in_gga(f, X1) → U55_gga(X1, delcI_in_ga(.(f, X1)))
delcI_in_ga(.(f, X1)) → delcI_out_ga(.(f, X1), X1)
U55_gga(X1, delcI_out_ga(.(f, X1), X2)) → delcE_out_gga(f, X1, .(t, X2))
delcD_in_gga(t, X1) → delcD_out_gga(t, X1, .(t, X1))
delcD_in_gga(f, X1) → U54_gga(X1, delcI_in_ga(X1))
delcI_in_ga([]) → delcI_out_ga([], [])
delcI_in_ga(.(t, X1)) → U50_ga(X1, delcI_in_ga(X1))
U54_gga(X1, delcI_out_ga(X1, X2)) → delcD_out_gga(f, X1, .(t, .(t, X2)))
U50_ga(X1, delcI_out_ga(X1, X2)) → delcI_out_ga(.(t, X1), .(t, X2))
maxcC_in_ga(x0)
delcD_in_gga(x0, x1)
delcE_in_gga(x0, x1)
maxcF_in_ga(x0)
delcG_in_gga(x0, x1)
delcH_in_gga(x0, x1)
U48_ga(x0, x1)
U49_ga(x0, x1)
U54_gga(x0, x1)
U55_gga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)
U56_gga(x0, x1)
U57_gga(x0, x1)
delcI_in_ga(x0)
delcJ_in_ga(x0)
U50_ga(x0, x1)
U53_ga(x0, x1)
U12_GA(X1, maxcC_out_ga(X1, X2)) → U13_GA(X1, delcD_in_gga(X2, X1))
U13_GA(X1, delcD_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(t, .(t, X1))) → U12_GA(X1, maxcC_in_ga(X1))
MAXSORTA_IN_GA(.(t, .(f, X1))) → U18_GA(X1, maxcC_in_ga(X1))
U18_GA(X1, maxcC_out_ga(X1, X2)) → U19_GA(X1, delcE_in_gga(X2, X1))
U19_GA(X1, delcE_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(f, .(f, X1))) → U24_GA(X1, maxcF_in_ga(X1))
U24_GA(X1, maxcF_out_ga(X1, X2)) → U25_GA(X1, delcG_in_gga(X2, X1))
U25_GA(X1, delcG_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(f, .(t, X1))) → U30_GA(X1, maxcC_in_ga(X1))
U30_GA(X1, maxcC_out_ga(X1, X2)) → U31_GA(X1, delcH_in_gga(X2, X1))
U31_GA(X1, delcH_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
delcH_in_gga(f, X1) → delcH_out_gga(f, X1, .(t, X1))
delcH_in_gga(t, X1) → U57_gga(X1, delcJ_in_ga(.(t, X1)))
delcJ_in_ga(.(t, X1)) → delcJ_out_ga(.(t, X1), X1)
U57_gga(X1, delcJ_out_ga(.(t, X1), X2)) → delcH_out_gga(t, X1, .(f, X2))
maxcC_in_ga([]) → maxcC_out_ga([], t)
maxcC_in_ga(.(t, X1)) → U48_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga(.(f, X1)) → U49_ga(X1, maxcC_in_ga(X1))
U49_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(f, X1), X2)
U48_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(t, X1), X2)
delcG_in_gga(f, X1) → delcG_out_gga(f, X1, .(f, X1))
delcG_in_gga(t, X1) → U56_gga(X1, delcJ_in_ga(X1))
delcJ_in_ga([]) → delcJ_out_ga([], [])
delcJ_in_ga(.(f, X1)) → U53_ga(X1, delcJ_in_ga(X1))
U56_gga(X1, delcJ_out_ga(X1, X2)) → delcG_out_gga(t, X1, .(f, .(f, X2)))
U53_ga(X1, delcJ_out_ga(X1, X2)) → delcJ_out_ga(.(f, X1), .(f, X2))
maxcF_in_ga([]) → maxcF_out_ga([], f)
maxcF_in_ga(.(f, X1)) → U51_ga(X1, maxcF_in_ga(X1))
maxcF_in_ga(.(t, X1)) → U52_ga(X1, maxcC_in_ga(X1))
U52_ga(X1, maxcC_out_ga(X1, X2)) → maxcF_out_ga(.(t, X1), X2)
U51_ga(X1, maxcF_out_ga(X1, X2)) → maxcF_out_ga(.(f, X1), X2)
delcE_in_gga(t, X1) → delcE_out_gga(t, X1, .(f, X1))
delcE_in_gga(f, X1) → U55_gga(X1, delcI_in_ga(.(f, X1)))
delcI_in_ga(.(f, X1)) → delcI_out_ga(.(f, X1), X1)
U55_gga(X1, delcI_out_ga(.(f, X1), X2)) → delcE_out_gga(f, X1, .(t, X2))
delcD_in_gga(t, X1) → delcD_out_gga(t, X1, .(t, X1))
delcD_in_gga(f, X1) → U54_gga(X1, delcI_in_ga(X1))
delcI_in_ga([]) → delcI_out_ga([], [])
delcI_in_ga(.(t, X1)) → U50_ga(X1, delcI_in_ga(X1))
U54_gga(X1, delcI_out_ga(X1, X2)) → delcD_out_gga(f, X1, .(t, .(t, X2)))
U50_ga(X1, delcI_out_ga(X1, X2)) → delcI_out_ga(.(t, X1), .(t, X2))
maxcC_in_ga(x0)
delcD_in_gga(x0, x1)
delcE_in_gga(x0, x1)
maxcF_in_ga(x0)
delcG_in_gga(x0, x1)
delcH_in_gga(x0, x1)
U48_ga(x0, x1)
U49_ga(x0, x1)
U54_gga(x0, x1)
U55_gga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)
U56_gga(x0, x1)
U57_gga(x0, x1)
delcI_in_ga(x0)
delcJ_in_ga(x0)
U50_ga(x0, x1)
U53_ga(x0, x1)
delcH_in_gga(f, X1) → delcH_out_gga(f, X1, .(t, X1))
POL(.(x1, x2)) = 0
POL(MAXSORTA_IN_GA(x1)) = 0
POL(U12_GA(x1, x2)) = 2·x2
POL(U13_GA(x1, x2)) = 0
POL(U18_GA(x1, x2)) = 0
POL(U19_GA(x1, x2)) = 0
POL(U24_GA(x1, x2)) = 0
POL(U25_GA(x1, x2)) = 0
POL(U30_GA(x1, x2)) = 2·x2
POL(U31_GA(x1, x2)) = x2
POL(U48_ga(x1, x2)) = x2
POL(U49_ga(x1, x2)) = 2·x2
POL(U50_ga(x1, x2)) = 0
POL(U51_ga(x1, x2)) = 0
POL(U52_ga(x1, x2)) = 0
POL(U53_ga(x1, x2)) = 2·x2
POL(U54_gga(x1, x2)) = 0
POL(U55_gga(x1, x2)) = x1
POL(U56_gga(x1, x2)) = 1 + x1
POL(U57_gga(x1, x2)) = 0
POL([]) = 0
POL(delcD_in_gga(x1, x2)) = 2·x1
POL(delcD_out_gga(x1, x2, x3)) = 0
POL(delcE_in_gga(x1, x2)) = x2
POL(delcE_out_gga(x1, x2, x3)) = x2
POL(delcG_in_gga(x1, x2)) = 2 + x2
POL(delcG_out_gga(x1, x2, x3)) = 1
POL(delcH_in_gga(x1, x2)) = x1
POL(delcH_out_gga(x1, x2, x3)) = 0
POL(delcI_in_ga(x1)) = 0
POL(delcI_out_ga(x1, x2)) = 0
POL(delcJ_in_ga(x1)) = 0
POL(delcJ_out_ga(x1, x2)) = 0
POL(f) = 2
POL(maxcC_in_ga(x1)) = 0
POL(maxcC_out_ga(x1, x2)) = 2·x1 + 2·x2
POL(maxcF_in_ga(x1)) = 0
POL(maxcF_out_ga(x1, x2)) = 0
POL(t) = 0
U12_GA(X1, maxcC_out_ga(X1, X2)) → U13_GA(X1, delcD_in_gga(X2, X1))
U13_GA(X1, delcD_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(t, .(t, X1))) → U12_GA(X1, maxcC_in_ga(X1))
MAXSORTA_IN_GA(.(t, .(f, X1))) → U18_GA(X1, maxcC_in_ga(X1))
U18_GA(X1, maxcC_out_ga(X1, X2)) → U19_GA(X1, delcE_in_gga(X2, X1))
U19_GA(X1, delcE_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(f, .(f, X1))) → U24_GA(X1, maxcF_in_ga(X1))
U24_GA(X1, maxcF_out_ga(X1, X2)) → U25_GA(X1, delcG_in_gga(X2, X1))
U25_GA(X1, delcG_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(f, .(t, X1))) → U30_GA(X1, maxcC_in_ga(X1))
U30_GA(X1, maxcC_out_ga(X1, X2)) → U31_GA(X1, delcH_in_gga(X2, X1))
U31_GA(X1, delcH_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
delcH_in_gga(t, X1) → U57_gga(X1, delcJ_in_ga(.(t, X1)))
delcJ_in_ga(.(t, X1)) → delcJ_out_ga(.(t, X1), X1)
U57_gga(X1, delcJ_out_ga(.(t, X1), X2)) → delcH_out_gga(t, X1, .(f, X2))
maxcC_in_ga([]) → maxcC_out_ga([], t)
maxcC_in_ga(.(t, X1)) → U48_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga(.(f, X1)) → U49_ga(X1, maxcC_in_ga(X1))
U49_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(f, X1), X2)
U48_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(t, X1), X2)
delcG_in_gga(f, X1) → delcG_out_gga(f, X1, .(f, X1))
delcG_in_gga(t, X1) → U56_gga(X1, delcJ_in_ga(X1))
delcJ_in_ga([]) → delcJ_out_ga([], [])
delcJ_in_ga(.(f, X1)) → U53_ga(X1, delcJ_in_ga(X1))
U56_gga(X1, delcJ_out_ga(X1, X2)) → delcG_out_gga(t, X1, .(f, .(f, X2)))
U53_ga(X1, delcJ_out_ga(X1, X2)) → delcJ_out_ga(.(f, X1), .(f, X2))
maxcF_in_ga([]) → maxcF_out_ga([], f)
maxcF_in_ga(.(f, X1)) → U51_ga(X1, maxcF_in_ga(X1))
maxcF_in_ga(.(t, X1)) → U52_ga(X1, maxcC_in_ga(X1))
U52_ga(X1, maxcC_out_ga(X1, X2)) → maxcF_out_ga(.(t, X1), X2)
U51_ga(X1, maxcF_out_ga(X1, X2)) → maxcF_out_ga(.(f, X1), X2)
delcE_in_gga(t, X1) → delcE_out_gga(t, X1, .(f, X1))
delcE_in_gga(f, X1) → U55_gga(X1, delcI_in_ga(.(f, X1)))
delcI_in_ga(.(f, X1)) → delcI_out_ga(.(f, X1), X1)
U55_gga(X1, delcI_out_ga(.(f, X1), X2)) → delcE_out_gga(f, X1, .(t, X2))
delcD_in_gga(t, X1) → delcD_out_gga(t, X1, .(t, X1))
delcD_in_gga(f, X1) → U54_gga(X1, delcI_in_ga(X1))
delcI_in_ga([]) → delcI_out_ga([], [])
delcI_in_ga(.(t, X1)) → U50_ga(X1, delcI_in_ga(X1))
U54_gga(X1, delcI_out_ga(X1, X2)) → delcD_out_gga(f, X1, .(t, .(t, X2)))
U50_ga(X1, delcI_out_ga(X1, X2)) → delcI_out_ga(.(t, X1), .(t, X2))
maxcC_in_ga(x0)
delcD_in_gga(x0, x1)
delcE_in_gga(x0, x1)
maxcF_in_ga(x0)
delcG_in_gga(x0, x1)
delcH_in_gga(x0, x1)
U48_ga(x0, x1)
U49_ga(x0, x1)
U54_gga(x0, x1)
U55_gga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)
U56_gga(x0, x1)
U57_gga(x0, x1)
delcI_in_ga(x0)
delcJ_in_ga(x0)
U50_ga(x0, x1)
U53_ga(x0, x1)
U55_gga(X1, delcI_out_ga(.(f, X1), X2)) → delcE_out_gga(f, X1, .(t, X2))
POL(.(x1, x2)) = 0
POL(MAXSORTA_IN_GA(x1)) = 0
POL(U12_GA(x1, x2)) = 0
POL(U13_GA(x1, x2)) = 0
POL(U18_GA(x1, x2)) = 2·x2
POL(U19_GA(x1, x2)) = x2
POL(U24_GA(x1, x2)) = 0
POL(U25_GA(x1, x2)) = 0
POL(U30_GA(x1, x2)) = 0
POL(U31_GA(x1, x2)) = 0
POL(U48_ga(x1, x2)) = x2
POL(U49_ga(x1, x2)) = x2
POL(U50_ga(x1, x2)) = 2
POL(U51_ga(x1, x2)) = 0
POL(U52_ga(x1, x2)) = 0
POL(U53_ga(x1, x2)) = 0
POL(U54_gga(x1, x2)) = x1
POL(U55_gga(x1, x2)) = 2·x2
POL(U56_gga(x1, x2)) = x1
POL(U57_gga(x1, x2)) = 1
POL([]) = 0
POL(delcD_in_gga(x1, x2)) = 2·x2
POL(delcD_out_gga(x1, x2, x3)) = x3
POL(delcE_in_gga(x1, x2)) = 2·x1
POL(delcE_out_gga(x1, x2, x3)) = 2·x3
POL(delcG_in_gga(x1, x2)) = 2 + 2·x2
POL(delcG_out_gga(x1, x2, x3)) = x3
POL(delcH_in_gga(x1, x2)) = 1
POL(delcH_out_gga(x1, x2, x3)) = 0
POL(delcI_in_ga(x1)) = 2
POL(delcI_out_ga(x1, x2)) = 1
POL(delcJ_in_ga(x1)) = 1
POL(delcJ_out_ga(x1, x2)) = 0
POL(f) = 2
POL(maxcC_in_ga(x1)) = 0
POL(maxcC_out_ga(x1, x2)) = x2
POL(maxcF_in_ga(x1)) = 0
POL(maxcF_out_ga(x1, x2)) = 0
POL(t) = 0
U12_GA(X1, maxcC_out_ga(X1, X2)) → U13_GA(X1, delcD_in_gga(X2, X1))
U13_GA(X1, delcD_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(t, .(t, X1))) → U12_GA(X1, maxcC_in_ga(X1))
MAXSORTA_IN_GA(.(t, .(f, X1))) → U18_GA(X1, maxcC_in_ga(X1))
U18_GA(X1, maxcC_out_ga(X1, X2)) → U19_GA(X1, delcE_in_gga(X2, X1))
U19_GA(X1, delcE_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(f, .(f, X1))) → U24_GA(X1, maxcF_in_ga(X1))
U24_GA(X1, maxcF_out_ga(X1, X2)) → U25_GA(X1, delcG_in_gga(X2, X1))
U25_GA(X1, delcG_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(f, .(t, X1))) → U30_GA(X1, maxcC_in_ga(X1))
U30_GA(X1, maxcC_out_ga(X1, X2)) → U31_GA(X1, delcH_in_gga(X2, X1))
U31_GA(X1, delcH_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
delcH_in_gga(t, X1) → U57_gga(X1, delcJ_in_ga(.(t, X1)))
delcJ_in_ga(.(t, X1)) → delcJ_out_ga(.(t, X1), X1)
U57_gga(X1, delcJ_out_ga(.(t, X1), X2)) → delcH_out_gga(t, X1, .(f, X2))
maxcC_in_ga([]) → maxcC_out_ga([], t)
maxcC_in_ga(.(t, X1)) → U48_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga(.(f, X1)) → U49_ga(X1, maxcC_in_ga(X1))
U49_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(f, X1), X2)
U48_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(t, X1), X2)
delcG_in_gga(f, X1) → delcG_out_gga(f, X1, .(f, X1))
delcG_in_gga(t, X1) → U56_gga(X1, delcJ_in_ga(X1))
delcJ_in_ga([]) → delcJ_out_ga([], [])
delcJ_in_ga(.(f, X1)) → U53_ga(X1, delcJ_in_ga(X1))
U56_gga(X1, delcJ_out_ga(X1, X2)) → delcG_out_gga(t, X1, .(f, .(f, X2)))
U53_ga(X1, delcJ_out_ga(X1, X2)) → delcJ_out_ga(.(f, X1), .(f, X2))
maxcF_in_ga([]) → maxcF_out_ga([], f)
maxcF_in_ga(.(f, X1)) → U51_ga(X1, maxcF_in_ga(X1))
maxcF_in_ga(.(t, X1)) → U52_ga(X1, maxcC_in_ga(X1))
U52_ga(X1, maxcC_out_ga(X1, X2)) → maxcF_out_ga(.(t, X1), X2)
U51_ga(X1, maxcF_out_ga(X1, X2)) → maxcF_out_ga(.(f, X1), X2)
delcE_in_gga(t, X1) → delcE_out_gga(t, X1, .(f, X1))
delcE_in_gga(f, X1) → U55_gga(X1, delcI_in_ga(.(f, X1)))
delcI_in_ga(.(f, X1)) → delcI_out_ga(.(f, X1), X1)
delcD_in_gga(t, X1) → delcD_out_gga(t, X1, .(t, X1))
delcD_in_gga(f, X1) → U54_gga(X1, delcI_in_ga(X1))
delcI_in_ga([]) → delcI_out_ga([], [])
delcI_in_ga(.(t, X1)) → U50_ga(X1, delcI_in_ga(X1))
U54_gga(X1, delcI_out_ga(X1, X2)) → delcD_out_gga(f, X1, .(t, .(t, X2)))
U50_ga(X1, delcI_out_ga(X1, X2)) → delcI_out_ga(.(t, X1), .(t, X2))
maxcC_in_ga(x0)
delcD_in_gga(x0, x1)
delcE_in_gga(x0, x1)
maxcF_in_ga(x0)
delcG_in_gga(x0, x1)
delcH_in_gga(x0, x1)
U48_ga(x0, x1)
U49_ga(x0, x1)
U54_gga(x0, x1)
U55_gga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)
U56_gga(x0, x1)
U57_gga(x0, x1)
delcI_in_ga(x0)
delcJ_in_ga(x0)
U50_ga(x0, x1)
U53_ga(x0, x1)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
MAXSORTA_IN_GA(.(t, .(f, X1))) → U18_GA(X1, maxcC_in_ga(X1))
POL(.(x1, x2)) = x1
POL(MAXSORTA_IN_GA(x1)) = x1
POL(U12_GA(x1, x2)) = 1
POL(U13_GA(x1, x2)) = x2
POL(U18_GA(x1, x2)) = 0
POL(U19_GA(x1, x2)) = x2
POL(U24_GA(x1, x2)) = 0
POL(U25_GA(x1, x2)) = x2
POL(U30_GA(x1, x2)) = 0
POL(U31_GA(x1, x2)) = x2
POL(U48_ga(x1, x2)) = 0
POL(U49_ga(x1, x2)) = 0
POL(U50_ga(x1, x2)) = 0
POL(U51_ga(x1, x2)) = 0
POL(U52_ga(x1, x2)) = 0
POL(U53_ga(x1, x2)) = 0
POL(U54_gga(x1, x2)) = 1
POL(U55_gga(x1, x2)) = 0
POL(U56_gga(x1, x2)) = 0
POL(U57_gga(x1, x2)) = 0
POL([]) = 0
POL(delcD_in_gga(x1, x2)) = 1
POL(delcD_out_gga(x1, x2, x3)) = x3
POL(delcE_in_gga(x1, x2)) = 0
POL(delcE_out_gga(x1, x2, x3)) = x3
POL(delcG_in_gga(x1, x2)) = 0
POL(delcG_out_gga(x1, x2, x3)) = x3
POL(delcH_in_gga(x1, x2)) = 0
POL(delcH_out_gga(x1, x2, x3)) = x3
POL(delcI_in_ga(x1)) = 0
POL(delcI_out_ga(x1, x2)) = 0
POL(delcJ_in_ga(x1)) = 0
POL(delcJ_out_ga(x1, x2)) = 0
POL(f) = 0
POL(maxcC_in_ga(x1)) = 0
POL(maxcC_out_ga(x1, x2)) = 0
POL(maxcF_in_ga(x1)) = 0
POL(maxcF_out_ga(x1, x2)) = 0
POL(t) = 1
delcD_in_gga(t, X1) → delcD_out_gga(t, X1, .(t, X1))
delcD_in_gga(f, X1) → U54_gga(X1, delcI_in_ga(X1))
delcE_in_gga(t, X1) → delcE_out_gga(t, X1, .(f, X1))
delcE_in_gga(f, X1) → U55_gga(X1, delcI_in_ga(.(f, X1)))
delcG_in_gga(f, X1) → delcG_out_gga(f, X1, .(f, X1))
delcG_in_gga(t, X1) → U56_gga(X1, delcJ_in_ga(X1))
delcH_in_gga(t, X1) → U57_gga(X1, delcJ_in_ga(.(t, X1)))
U57_gga(X1, delcJ_out_ga(.(t, X1), X2)) → delcH_out_gga(t, X1, .(f, X2))
U56_gga(X1, delcJ_out_ga(X1, X2)) → delcG_out_gga(t, X1, .(f, .(f, X2)))
U54_gga(X1, delcI_out_ga(X1, X2)) → delcD_out_gga(f, X1, .(t, .(t, X2)))
U12_GA(X1, maxcC_out_ga(X1, X2)) → U13_GA(X1, delcD_in_gga(X2, X1))
U13_GA(X1, delcD_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(t, .(t, X1))) → U12_GA(X1, maxcC_in_ga(X1))
U18_GA(X1, maxcC_out_ga(X1, X2)) → U19_GA(X1, delcE_in_gga(X2, X1))
U19_GA(X1, delcE_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(f, .(f, X1))) → U24_GA(X1, maxcF_in_ga(X1))
U24_GA(X1, maxcF_out_ga(X1, X2)) → U25_GA(X1, delcG_in_gga(X2, X1))
U25_GA(X1, delcG_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(f, .(t, X1))) → U30_GA(X1, maxcC_in_ga(X1))
U30_GA(X1, maxcC_out_ga(X1, X2)) → U31_GA(X1, delcH_in_gga(X2, X1))
U31_GA(X1, delcH_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
delcH_in_gga(t, X1) → U57_gga(X1, delcJ_in_ga(.(t, X1)))
delcJ_in_ga(.(t, X1)) → delcJ_out_ga(.(t, X1), X1)
U57_gga(X1, delcJ_out_ga(.(t, X1), X2)) → delcH_out_gga(t, X1, .(f, X2))
maxcC_in_ga([]) → maxcC_out_ga([], t)
maxcC_in_ga(.(t, X1)) → U48_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga(.(f, X1)) → U49_ga(X1, maxcC_in_ga(X1))
U49_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(f, X1), X2)
U48_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(t, X1), X2)
delcG_in_gga(f, X1) → delcG_out_gga(f, X1, .(f, X1))
delcG_in_gga(t, X1) → U56_gga(X1, delcJ_in_ga(X1))
delcJ_in_ga([]) → delcJ_out_ga([], [])
delcJ_in_ga(.(f, X1)) → U53_ga(X1, delcJ_in_ga(X1))
U56_gga(X1, delcJ_out_ga(X1, X2)) → delcG_out_gga(t, X1, .(f, .(f, X2)))
U53_ga(X1, delcJ_out_ga(X1, X2)) → delcJ_out_ga(.(f, X1), .(f, X2))
maxcF_in_ga([]) → maxcF_out_ga([], f)
maxcF_in_ga(.(f, X1)) → U51_ga(X1, maxcF_in_ga(X1))
maxcF_in_ga(.(t, X1)) → U52_ga(X1, maxcC_in_ga(X1))
U52_ga(X1, maxcC_out_ga(X1, X2)) → maxcF_out_ga(.(t, X1), X2)
U51_ga(X1, maxcF_out_ga(X1, X2)) → maxcF_out_ga(.(f, X1), X2)
delcE_in_gga(t, X1) → delcE_out_gga(t, X1, .(f, X1))
delcE_in_gga(f, X1) → U55_gga(X1, delcI_in_ga(.(f, X1)))
delcI_in_ga(.(f, X1)) → delcI_out_ga(.(f, X1), X1)
delcD_in_gga(t, X1) → delcD_out_gga(t, X1, .(t, X1))
delcD_in_gga(f, X1) → U54_gga(X1, delcI_in_ga(X1))
delcI_in_ga([]) → delcI_out_ga([], [])
delcI_in_ga(.(t, X1)) → U50_ga(X1, delcI_in_ga(X1))
U54_gga(X1, delcI_out_ga(X1, X2)) → delcD_out_gga(f, X1, .(t, .(t, X2)))
U50_ga(X1, delcI_out_ga(X1, X2)) → delcI_out_ga(.(t, X1), .(t, X2))
maxcC_in_ga(x0)
delcD_in_gga(x0, x1)
delcE_in_gga(x0, x1)
maxcF_in_ga(x0)
delcG_in_gga(x0, x1)
delcH_in_gga(x0, x1)
U48_ga(x0, x1)
U49_ga(x0, x1)
U54_gga(x0, x1)
U55_gga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)
U56_gga(x0, x1)
U57_gga(x0, x1)
delcI_in_ga(x0)
delcJ_in_ga(x0)
U50_ga(x0, x1)
U53_ga(x0, x1)
U13_GA(X1, delcD_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(t, .(t, X1))) → U12_GA(X1, maxcC_in_ga(X1))
U12_GA(X1, maxcC_out_ga(X1, X2)) → U13_GA(X1, delcD_in_gga(X2, X1))
MAXSORTA_IN_GA(.(f, .(f, X1))) → U24_GA(X1, maxcF_in_ga(X1))
U24_GA(X1, maxcF_out_ga(X1, X2)) → U25_GA(X1, delcG_in_gga(X2, X1))
U25_GA(X1, delcG_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(f, .(t, X1))) → U30_GA(X1, maxcC_in_ga(X1))
U30_GA(X1, maxcC_out_ga(X1, X2)) → U31_GA(X1, delcH_in_gga(X2, X1))
U31_GA(X1, delcH_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
delcH_in_gga(t, X1) → U57_gga(X1, delcJ_in_ga(.(t, X1)))
delcJ_in_ga(.(t, X1)) → delcJ_out_ga(.(t, X1), X1)
U57_gga(X1, delcJ_out_ga(.(t, X1), X2)) → delcH_out_gga(t, X1, .(f, X2))
maxcC_in_ga([]) → maxcC_out_ga([], t)
maxcC_in_ga(.(t, X1)) → U48_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga(.(f, X1)) → U49_ga(X1, maxcC_in_ga(X1))
U49_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(f, X1), X2)
U48_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(t, X1), X2)
delcG_in_gga(f, X1) → delcG_out_gga(f, X1, .(f, X1))
delcG_in_gga(t, X1) → U56_gga(X1, delcJ_in_ga(X1))
delcJ_in_ga([]) → delcJ_out_ga([], [])
delcJ_in_ga(.(f, X1)) → U53_ga(X1, delcJ_in_ga(X1))
U56_gga(X1, delcJ_out_ga(X1, X2)) → delcG_out_gga(t, X1, .(f, .(f, X2)))
U53_ga(X1, delcJ_out_ga(X1, X2)) → delcJ_out_ga(.(f, X1), .(f, X2))
maxcF_in_ga([]) → maxcF_out_ga([], f)
maxcF_in_ga(.(f, X1)) → U51_ga(X1, maxcF_in_ga(X1))
maxcF_in_ga(.(t, X1)) → U52_ga(X1, maxcC_in_ga(X1))
U52_ga(X1, maxcC_out_ga(X1, X2)) → maxcF_out_ga(.(t, X1), X2)
U51_ga(X1, maxcF_out_ga(X1, X2)) → maxcF_out_ga(.(f, X1), X2)
delcE_in_gga(t, X1) → delcE_out_gga(t, X1, .(f, X1))
delcE_in_gga(f, X1) → U55_gga(X1, delcI_in_ga(.(f, X1)))
delcI_in_ga(.(f, X1)) → delcI_out_ga(.(f, X1), X1)
delcD_in_gga(t, X1) → delcD_out_gga(t, X1, .(t, X1))
delcD_in_gga(f, X1) → U54_gga(X1, delcI_in_ga(X1))
delcI_in_ga([]) → delcI_out_ga([], [])
delcI_in_ga(.(t, X1)) → U50_ga(X1, delcI_in_ga(X1))
U54_gga(X1, delcI_out_ga(X1, X2)) → delcD_out_gga(f, X1, .(t, .(t, X2)))
U50_ga(X1, delcI_out_ga(X1, X2)) → delcI_out_ga(.(t, X1), .(t, X2))
maxcC_in_ga(x0)
delcD_in_gga(x0, x1)
delcE_in_gga(x0, x1)
maxcF_in_ga(x0)
delcG_in_gga(x0, x1)
delcH_in_gga(x0, x1)
U48_ga(x0, x1)
U49_ga(x0, x1)
U54_gga(x0, x1)
U55_gga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)
U56_gga(x0, x1)
U57_gga(x0, x1)
delcI_in_ga(x0)
delcJ_in_ga(x0)
U50_ga(x0, x1)
U53_ga(x0, x1)
U13_GA(X1, delcD_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(t, .(t, X1))) → U12_GA(X1, maxcC_in_ga(X1))
U12_GA(X1, maxcC_out_ga(X1, X2)) → U13_GA(X1, delcD_in_gga(X2, X1))
MAXSORTA_IN_GA(.(f, .(f, X1))) → U24_GA(X1, maxcF_in_ga(X1))
U24_GA(X1, maxcF_out_ga(X1, X2)) → U25_GA(X1, delcG_in_gga(X2, X1))
U25_GA(X1, delcG_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(f, .(t, X1))) → U30_GA(X1, maxcC_in_ga(X1))
U30_GA(X1, maxcC_out_ga(X1, X2)) → U31_GA(X1, delcH_in_gga(X2, X1))
U31_GA(X1, delcH_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
delcH_in_gga(t, X1) → U57_gga(X1, delcJ_in_ga(.(t, X1)))
delcJ_in_ga(.(t, X1)) → delcJ_out_ga(.(t, X1), X1)
U57_gga(X1, delcJ_out_ga(.(t, X1), X2)) → delcH_out_gga(t, X1, .(f, X2))
maxcC_in_ga([]) → maxcC_out_ga([], t)
maxcC_in_ga(.(t, X1)) → U48_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga(.(f, X1)) → U49_ga(X1, maxcC_in_ga(X1))
U49_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(f, X1), X2)
U48_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(t, X1), X2)
delcG_in_gga(f, X1) → delcG_out_gga(f, X1, .(f, X1))
delcG_in_gga(t, X1) → U56_gga(X1, delcJ_in_ga(X1))
delcJ_in_ga([]) → delcJ_out_ga([], [])
delcJ_in_ga(.(f, X1)) → U53_ga(X1, delcJ_in_ga(X1))
U56_gga(X1, delcJ_out_ga(X1, X2)) → delcG_out_gga(t, X1, .(f, .(f, X2)))
U53_ga(X1, delcJ_out_ga(X1, X2)) → delcJ_out_ga(.(f, X1), .(f, X2))
maxcF_in_ga([]) → maxcF_out_ga([], f)
maxcF_in_ga(.(f, X1)) → U51_ga(X1, maxcF_in_ga(X1))
maxcF_in_ga(.(t, X1)) → U52_ga(X1, maxcC_in_ga(X1))
U52_ga(X1, maxcC_out_ga(X1, X2)) → maxcF_out_ga(.(t, X1), X2)
U51_ga(X1, maxcF_out_ga(X1, X2)) → maxcF_out_ga(.(f, X1), X2)
delcD_in_gga(t, X1) → delcD_out_gga(t, X1, .(t, X1))
delcD_in_gga(f, X1) → U54_gga(X1, delcI_in_ga(X1))
delcI_in_ga(.(f, X1)) → delcI_out_ga(.(f, X1), X1)
delcI_in_ga([]) → delcI_out_ga([], [])
delcI_in_ga(.(t, X1)) → U50_ga(X1, delcI_in_ga(X1))
U54_gga(X1, delcI_out_ga(X1, X2)) → delcD_out_gga(f, X1, .(t, .(t, X2)))
U50_ga(X1, delcI_out_ga(X1, X2)) → delcI_out_ga(.(t, X1), .(t, X2))
maxcC_in_ga(x0)
delcD_in_gga(x0, x1)
delcE_in_gga(x0, x1)
maxcF_in_ga(x0)
delcG_in_gga(x0, x1)
delcH_in_gga(x0, x1)
U48_ga(x0, x1)
U49_ga(x0, x1)
U54_gga(x0, x1)
U55_gga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)
U56_gga(x0, x1)
U57_gga(x0, x1)
delcI_in_ga(x0)
delcJ_in_ga(x0)
U50_ga(x0, x1)
U53_ga(x0, x1)
delcE_in_gga(x0, x1)
U55_gga(x0, x1)
U13_GA(X1, delcD_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(t, .(t, X1))) → U12_GA(X1, maxcC_in_ga(X1))
U12_GA(X1, maxcC_out_ga(X1, X2)) → U13_GA(X1, delcD_in_gga(X2, X1))
MAXSORTA_IN_GA(.(f, .(f, X1))) → U24_GA(X1, maxcF_in_ga(X1))
U24_GA(X1, maxcF_out_ga(X1, X2)) → U25_GA(X1, delcG_in_gga(X2, X1))
U25_GA(X1, delcG_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(f, .(t, X1))) → U30_GA(X1, maxcC_in_ga(X1))
U30_GA(X1, maxcC_out_ga(X1, X2)) → U31_GA(X1, delcH_in_gga(X2, X1))
U31_GA(X1, delcH_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
delcH_in_gga(t, X1) → U57_gga(X1, delcJ_in_ga(.(t, X1)))
delcJ_in_ga(.(t, X1)) → delcJ_out_ga(.(t, X1), X1)
U57_gga(X1, delcJ_out_ga(.(t, X1), X2)) → delcH_out_gga(t, X1, .(f, X2))
maxcC_in_ga([]) → maxcC_out_ga([], t)
maxcC_in_ga(.(t, X1)) → U48_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga(.(f, X1)) → U49_ga(X1, maxcC_in_ga(X1))
U49_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(f, X1), X2)
U48_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(t, X1), X2)
delcG_in_gga(f, X1) → delcG_out_gga(f, X1, .(f, X1))
delcG_in_gga(t, X1) → U56_gga(X1, delcJ_in_ga(X1))
delcJ_in_ga([]) → delcJ_out_ga([], [])
delcJ_in_ga(.(f, X1)) → U53_ga(X1, delcJ_in_ga(X1))
U56_gga(X1, delcJ_out_ga(X1, X2)) → delcG_out_gga(t, X1, .(f, .(f, X2)))
U53_ga(X1, delcJ_out_ga(X1, X2)) → delcJ_out_ga(.(f, X1), .(f, X2))
maxcF_in_ga([]) → maxcF_out_ga([], f)
maxcF_in_ga(.(f, X1)) → U51_ga(X1, maxcF_in_ga(X1))
maxcF_in_ga(.(t, X1)) → U52_ga(X1, maxcC_in_ga(X1))
U52_ga(X1, maxcC_out_ga(X1, X2)) → maxcF_out_ga(.(t, X1), X2)
U51_ga(X1, maxcF_out_ga(X1, X2)) → maxcF_out_ga(.(f, X1), X2)
delcD_in_gga(t, X1) → delcD_out_gga(t, X1, .(t, X1))
delcD_in_gga(f, X1) → U54_gga(X1, delcI_in_ga(X1))
delcI_in_ga(.(f, X1)) → delcI_out_ga(.(f, X1), X1)
delcI_in_ga([]) → delcI_out_ga([], [])
delcI_in_ga(.(t, X1)) → U50_ga(X1, delcI_in_ga(X1))
U54_gga(X1, delcI_out_ga(X1, X2)) → delcD_out_gga(f, X1, .(t, .(t, X2)))
U50_ga(X1, delcI_out_ga(X1, X2)) → delcI_out_ga(.(t, X1), .(t, X2))
maxcC_in_ga(x0)
delcD_in_gga(x0, x1)
maxcF_in_ga(x0)
delcG_in_gga(x0, x1)
delcH_in_gga(x0, x1)
U48_ga(x0, x1)
U49_ga(x0, x1)
U54_gga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)
U56_gga(x0, x1)
U57_gga(x0, x1)
delcI_in_ga(x0)
delcJ_in_ga(x0)
U50_ga(x0, x1)
U53_ga(x0, x1)
U54_gga(X1, delcI_out_ga(X1, X2)) → delcD_out_gga(f, X1, .(t, .(t, X2)))
POL(.(x1, x2)) = 0
POL(MAXSORTA_IN_GA(x1)) = 0
POL(U12_GA(x1, x2)) = 2·x2
POL(U13_GA(x1, x2)) = x2
POL(U24_GA(x1, x2)) = 0
POL(U25_GA(x1, x2)) = 0
POL(U30_GA(x1, x2)) = 0
POL(U31_GA(x1, x2)) = 0
POL(U48_ga(x1, x2)) = 2·x2
POL(U49_ga(x1, x2)) = x2
POL(U50_ga(x1, x2)) = 0
POL(U51_ga(x1, x2)) = 0
POL(U52_ga(x1, x2)) = 0
POL(U53_ga(x1, x2)) = 1
POL(U54_gga(x1, x2)) = 2
POL(U56_gga(x1, x2)) = 2·x1
POL(U57_gga(x1, x2)) = 0
POL([]) = 0
POL(delcD_in_gga(x1, x2)) = x1
POL(delcD_out_gga(x1, x2, x3)) = 0
POL(delcG_in_gga(x1, x2)) = 2·x2
POL(delcG_out_gga(x1, x2, x3)) = x2
POL(delcH_in_gga(x1, x2)) = 1
POL(delcH_out_gga(x1, x2, x3)) = x1
POL(delcI_in_ga(x1)) = 0
POL(delcI_out_ga(x1, x2)) = 2·x1
POL(delcJ_in_ga(x1)) = 2
POL(delcJ_out_ga(x1, x2)) = 1
POL(f) = 2
POL(maxcC_in_ga(x1)) = 0
POL(maxcC_out_ga(x1, x2)) = 2·x2
POL(maxcF_in_ga(x1)) = 0
POL(maxcF_out_ga(x1, x2)) = 2·x1
POL(t) = 0
U13_GA(X1, delcD_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(t, .(t, X1))) → U12_GA(X1, maxcC_in_ga(X1))
U12_GA(X1, maxcC_out_ga(X1, X2)) → U13_GA(X1, delcD_in_gga(X2, X1))
MAXSORTA_IN_GA(.(f, .(f, X1))) → U24_GA(X1, maxcF_in_ga(X1))
U24_GA(X1, maxcF_out_ga(X1, X2)) → U25_GA(X1, delcG_in_gga(X2, X1))
U25_GA(X1, delcG_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(f, .(t, X1))) → U30_GA(X1, maxcC_in_ga(X1))
U30_GA(X1, maxcC_out_ga(X1, X2)) → U31_GA(X1, delcH_in_gga(X2, X1))
U31_GA(X1, delcH_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
delcH_in_gga(t, X1) → U57_gga(X1, delcJ_in_ga(.(t, X1)))
delcJ_in_ga(.(t, X1)) → delcJ_out_ga(.(t, X1), X1)
U57_gga(X1, delcJ_out_ga(.(t, X1), X2)) → delcH_out_gga(t, X1, .(f, X2))
maxcC_in_ga([]) → maxcC_out_ga([], t)
maxcC_in_ga(.(t, X1)) → U48_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga(.(f, X1)) → U49_ga(X1, maxcC_in_ga(X1))
U49_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(f, X1), X2)
U48_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(t, X1), X2)
delcG_in_gga(f, X1) → delcG_out_gga(f, X1, .(f, X1))
delcG_in_gga(t, X1) → U56_gga(X1, delcJ_in_ga(X1))
delcJ_in_ga([]) → delcJ_out_ga([], [])
delcJ_in_ga(.(f, X1)) → U53_ga(X1, delcJ_in_ga(X1))
U56_gga(X1, delcJ_out_ga(X1, X2)) → delcG_out_gga(t, X1, .(f, .(f, X2)))
U53_ga(X1, delcJ_out_ga(X1, X2)) → delcJ_out_ga(.(f, X1), .(f, X2))
maxcF_in_ga([]) → maxcF_out_ga([], f)
maxcF_in_ga(.(f, X1)) → U51_ga(X1, maxcF_in_ga(X1))
maxcF_in_ga(.(t, X1)) → U52_ga(X1, maxcC_in_ga(X1))
U52_ga(X1, maxcC_out_ga(X1, X2)) → maxcF_out_ga(.(t, X1), X2)
U51_ga(X1, maxcF_out_ga(X1, X2)) → maxcF_out_ga(.(f, X1), X2)
delcD_in_gga(t, X1) → delcD_out_gga(t, X1, .(t, X1))
delcD_in_gga(f, X1) → U54_gga(X1, delcI_in_ga(X1))
delcI_in_ga(.(f, X1)) → delcI_out_ga(.(f, X1), X1)
delcI_in_ga([]) → delcI_out_ga([], [])
delcI_in_ga(.(t, X1)) → U50_ga(X1, delcI_in_ga(X1))
U50_ga(X1, delcI_out_ga(X1, X2)) → delcI_out_ga(.(t, X1), .(t, X2))
maxcC_in_ga(x0)
delcD_in_gga(x0, x1)
maxcF_in_ga(x0)
delcG_in_gga(x0, x1)
delcH_in_gga(x0, x1)
U48_ga(x0, x1)
U49_ga(x0, x1)
U54_gga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)
U56_gga(x0, x1)
U57_gga(x0, x1)
delcI_in_ga(x0)
delcJ_in_ga(x0)
U50_ga(x0, x1)
U53_ga(x0, x1)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
MAXSORTA_IN_GA(.(t, .(t, X1))) → U12_GA(X1, maxcC_in_ga(X1))
POL(.(x1, x2)) = x1 + x2
POL(MAXSORTA_IN_GA(x1)) = x1
POL(U12_GA(x1, x2)) = 1 + x1
POL(U13_GA(x1, x2)) = x2
POL(U24_GA(x1, x2)) = x1
POL(U25_GA(x1, x2)) = x2
POL(U30_GA(x1, x2)) = 1 + x1
POL(U31_GA(x1, x2)) = x2
POL(U48_ga(x1, x2)) = 0
POL(U49_ga(x1, x2)) = 0
POL(U50_ga(x1, x2)) = 0
POL(U51_ga(x1, x2)) = 0
POL(U52_ga(x1, x2)) = 0
POL(U53_ga(x1, x2)) = x2
POL(U54_gga(x1, x2)) = 0
POL(U56_gga(x1, x2)) = x2
POL(U57_gga(x1, x2)) = x2
POL([]) = 0
POL(delcD_in_gga(x1, x2)) = 1 + x2
POL(delcD_out_gga(x1, x2, x3)) = x3
POL(delcG_in_gga(x1, x2)) = x2
POL(delcG_out_gga(x1, x2, x3)) = x3
POL(delcH_in_gga(x1, x2)) = 1 + x2
POL(delcH_out_gga(x1, x2, x3)) = x3
POL(delcI_in_ga(x1)) = 0
POL(delcI_out_ga(x1, x2)) = 0
POL(delcJ_in_ga(x1)) = x1
POL(delcJ_out_ga(x1, x2)) = x2
POL(f) = 0
POL(maxcC_in_ga(x1)) = 0
POL(maxcC_out_ga(x1, x2)) = 0
POL(maxcF_in_ga(x1)) = 0
POL(maxcF_out_ga(x1, x2)) = 0
POL(t) = 1
delcD_in_gga(t, X1) → delcD_out_gga(t, X1, .(t, X1))
delcD_in_gga(f, X1) → U54_gga(X1, delcI_in_ga(X1))
delcG_in_gga(f, X1) → delcG_out_gga(f, X1, .(f, X1))
delcG_in_gga(t, X1) → U56_gga(X1, delcJ_in_ga(X1))
delcH_in_gga(t, X1) → U57_gga(X1, delcJ_in_ga(.(t, X1)))
delcJ_in_ga(.(t, X1)) → delcJ_out_ga(.(t, X1), X1)
U57_gga(X1, delcJ_out_ga(.(t, X1), X2)) → delcH_out_gga(t, X1, .(f, X2))
delcJ_in_ga([]) → delcJ_out_ga([], [])
delcJ_in_ga(.(f, X1)) → U53_ga(X1, delcJ_in_ga(X1))
U56_gga(X1, delcJ_out_ga(X1, X2)) → delcG_out_gga(t, X1, .(f, .(f, X2)))
U53_ga(X1, delcJ_out_ga(X1, X2)) → delcJ_out_ga(.(f, X1), .(f, X2))
U13_GA(X1, delcD_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
U12_GA(X1, maxcC_out_ga(X1, X2)) → U13_GA(X1, delcD_in_gga(X2, X1))
MAXSORTA_IN_GA(.(f, .(f, X1))) → U24_GA(X1, maxcF_in_ga(X1))
U24_GA(X1, maxcF_out_ga(X1, X2)) → U25_GA(X1, delcG_in_gga(X2, X1))
U25_GA(X1, delcG_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(f, .(t, X1))) → U30_GA(X1, maxcC_in_ga(X1))
U30_GA(X1, maxcC_out_ga(X1, X2)) → U31_GA(X1, delcH_in_gga(X2, X1))
U31_GA(X1, delcH_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
delcH_in_gga(t, X1) → U57_gga(X1, delcJ_in_ga(.(t, X1)))
delcJ_in_ga(.(t, X1)) → delcJ_out_ga(.(t, X1), X1)
U57_gga(X1, delcJ_out_ga(.(t, X1), X2)) → delcH_out_gga(t, X1, .(f, X2))
maxcC_in_ga([]) → maxcC_out_ga([], t)
maxcC_in_ga(.(t, X1)) → U48_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga(.(f, X1)) → U49_ga(X1, maxcC_in_ga(X1))
U49_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(f, X1), X2)
U48_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(t, X1), X2)
delcG_in_gga(f, X1) → delcG_out_gga(f, X1, .(f, X1))
delcG_in_gga(t, X1) → U56_gga(X1, delcJ_in_ga(X1))
delcJ_in_ga([]) → delcJ_out_ga([], [])
delcJ_in_ga(.(f, X1)) → U53_ga(X1, delcJ_in_ga(X1))
U56_gga(X1, delcJ_out_ga(X1, X2)) → delcG_out_gga(t, X1, .(f, .(f, X2)))
U53_ga(X1, delcJ_out_ga(X1, X2)) → delcJ_out_ga(.(f, X1), .(f, X2))
maxcF_in_ga([]) → maxcF_out_ga([], f)
maxcF_in_ga(.(f, X1)) → U51_ga(X1, maxcF_in_ga(X1))
maxcF_in_ga(.(t, X1)) → U52_ga(X1, maxcC_in_ga(X1))
U52_ga(X1, maxcC_out_ga(X1, X2)) → maxcF_out_ga(.(t, X1), X2)
U51_ga(X1, maxcF_out_ga(X1, X2)) → maxcF_out_ga(.(f, X1), X2)
delcD_in_gga(t, X1) → delcD_out_gga(t, X1, .(t, X1))
delcD_in_gga(f, X1) → U54_gga(X1, delcI_in_ga(X1))
delcI_in_ga(.(f, X1)) → delcI_out_ga(.(f, X1), X1)
delcI_in_ga([]) → delcI_out_ga([], [])
delcI_in_ga(.(t, X1)) → U50_ga(X1, delcI_in_ga(X1))
U50_ga(X1, delcI_out_ga(X1, X2)) → delcI_out_ga(.(t, X1), .(t, X2))
maxcC_in_ga(x0)
delcD_in_gga(x0, x1)
maxcF_in_ga(x0)
delcG_in_gga(x0, x1)
delcH_in_gga(x0, x1)
U48_ga(x0, x1)
U49_ga(x0, x1)
U54_gga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)
U56_gga(x0, x1)
U57_gga(x0, x1)
delcI_in_ga(x0)
delcJ_in_ga(x0)
U50_ga(x0, x1)
U53_ga(x0, x1)
U24_GA(X1, maxcF_out_ga(X1, X2)) → U25_GA(X1, delcG_in_gga(X2, X1))
U25_GA(X1, delcG_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(f, .(f, X1))) → U24_GA(X1, maxcF_in_ga(X1))
MAXSORTA_IN_GA(.(f, .(t, X1))) → U30_GA(X1, maxcC_in_ga(X1))
U30_GA(X1, maxcC_out_ga(X1, X2)) → U31_GA(X1, delcH_in_gga(X2, X1))
U31_GA(X1, delcH_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
delcH_in_gga(t, X1) → U57_gga(X1, delcJ_in_ga(.(t, X1)))
delcJ_in_ga(.(t, X1)) → delcJ_out_ga(.(t, X1), X1)
U57_gga(X1, delcJ_out_ga(.(t, X1), X2)) → delcH_out_gga(t, X1, .(f, X2))
maxcC_in_ga([]) → maxcC_out_ga([], t)
maxcC_in_ga(.(t, X1)) → U48_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga(.(f, X1)) → U49_ga(X1, maxcC_in_ga(X1))
U49_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(f, X1), X2)
U48_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(t, X1), X2)
delcG_in_gga(f, X1) → delcG_out_gga(f, X1, .(f, X1))
delcG_in_gga(t, X1) → U56_gga(X1, delcJ_in_ga(X1))
delcJ_in_ga([]) → delcJ_out_ga([], [])
delcJ_in_ga(.(f, X1)) → U53_ga(X1, delcJ_in_ga(X1))
U56_gga(X1, delcJ_out_ga(X1, X2)) → delcG_out_gga(t, X1, .(f, .(f, X2)))
U53_ga(X1, delcJ_out_ga(X1, X2)) → delcJ_out_ga(.(f, X1), .(f, X2))
maxcF_in_ga([]) → maxcF_out_ga([], f)
maxcF_in_ga(.(f, X1)) → U51_ga(X1, maxcF_in_ga(X1))
maxcF_in_ga(.(t, X1)) → U52_ga(X1, maxcC_in_ga(X1))
U52_ga(X1, maxcC_out_ga(X1, X2)) → maxcF_out_ga(.(t, X1), X2)
U51_ga(X1, maxcF_out_ga(X1, X2)) → maxcF_out_ga(.(f, X1), X2)
delcD_in_gga(t, X1) → delcD_out_gga(t, X1, .(t, X1))
delcD_in_gga(f, X1) → U54_gga(X1, delcI_in_ga(X1))
delcI_in_ga(.(f, X1)) → delcI_out_ga(.(f, X1), X1)
delcI_in_ga([]) → delcI_out_ga([], [])
delcI_in_ga(.(t, X1)) → U50_ga(X1, delcI_in_ga(X1))
U50_ga(X1, delcI_out_ga(X1, X2)) → delcI_out_ga(.(t, X1), .(t, X2))
maxcC_in_ga(x0)
delcD_in_gga(x0, x1)
maxcF_in_ga(x0)
delcG_in_gga(x0, x1)
delcH_in_gga(x0, x1)
U48_ga(x0, x1)
U49_ga(x0, x1)
U54_gga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)
U56_gga(x0, x1)
U57_gga(x0, x1)
delcI_in_ga(x0)
delcJ_in_ga(x0)
U50_ga(x0, x1)
U53_ga(x0, x1)
U24_GA(X1, maxcF_out_ga(X1, X2)) → U25_GA(X1, delcG_in_gga(X2, X1))
U25_GA(X1, delcG_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(f, .(f, X1))) → U24_GA(X1, maxcF_in_ga(X1))
MAXSORTA_IN_GA(.(f, .(t, X1))) → U30_GA(X1, maxcC_in_ga(X1))
U30_GA(X1, maxcC_out_ga(X1, X2)) → U31_GA(X1, delcH_in_gga(X2, X1))
U31_GA(X1, delcH_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
delcH_in_gga(t, X1) → U57_gga(X1, delcJ_in_ga(.(t, X1)))
delcJ_in_ga(.(t, X1)) → delcJ_out_ga(.(t, X1), X1)
U57_gga(X1, delcJ_out_ga(.(t, X1), X2)) → delcH_out_gga(t, X1, .(f, X2))
maxcC_in_ga([]) → maxcC_out_ga([], t)
maxcC_in_ga(.(t, X1)) → U48_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga(.(f, X1)) → U49_ga(X1, maxcC_in_ga(X1))
U49_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(f, X1), X2)
U48_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(t, X1), X2)
maxcF_in_ga([]) → maxcF_out_ga([], f)
maxcF_in_ga(.(f, X1)) → U51_ga(X1, maxcF_in_ga(X1))
maxcF_in_ga(.(t, X1)) → U52_ga(X1, maxcC_in_ga(X1))
U52_ga(X1, maxcC_out_ga(X1, X2)) → maxcF_out_ga(.(t, X1), X2)
U51_ga(X1, maxcF_out_ga(X1, X2)) → maxcF_out_ga(.(f, X1), X2)
delcG_in_gga(f, X1) → delcG_out_gga(f, X1, .(f, X1))
delcG_in_gga(t, X1) → U56_gga(X1, delcJ_in_ga(X1))
delcJ_in_ga([]) → delcJ_out_ga([], [])
delcJ_in_ga(.(f, X1)) → U53_ga(X1, delcJ_in_ga(X1))
U56_gga(X1, delcJ_out_ga(X1, X2)) → delcG_out_gga(t, X1, .(f, .(f, X2)))
U53_ga(X1, delcJ_out_ga(X1, X2)) → delcJ_out_ga(.(f, X1), .(f, X2))
maxcC_in_ga(x0)
delcD_in_gga(x0, x1)
maxcF_in_ga(x0)
delcG_in_gga(x0, x1)
delcH_in_gga(x0, x1)
U48_ga(x0, x1)
U49_ga(x0, x1)
U54_gga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)
U56_gga(x0, x1)
U57_gga(x0, x1)
delcI_in_ga(x0)
delcJ_in_ga(x0)
U50_ga(x0, x1)
U53_ga(x0, x1)
delcD_in_gga(x0, x1)
U54_gga(x0, x1)
delcI_in_ga(x0)
U50_ga(x0, x1)
U24_GA(X1, maxcF_out_ga(X1, X2)) → U25_GA(X1, delcG_in_gga(X2, X1))
U25_GA(X1, delcG_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(f, .(f, X1))) → U24_GA(X1, maxcF_in_ga(X1))
MAXSORTA_IN_GA(.(f, .(t, X1))) → U30_GA(X1, maxcC_in_ga(X1))
U30_GA(X1, maxcC_out_ga(X1, X2)) → U31_GA(X1, delcH_in_gga(X2, X1))
U31_GA(X1, delcH_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
delcH_in_gga(t, X1) → U57_gga(X1, delcJ_in_ga(.(t, X1)))
delcJ_in_ga(.(t, X1)) → delcJ_out_ga(.(t, X1), X1)
U57_gga(X1, delcJ_out_ga(.(t, X1), X2)) → delcH_out_gga(t, X1, .(f, X2))
maxcC_in_ga([]) → maxcC_out_ga([], t)
maxcC_in_ga(.(t, X1)) → U48_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga(.(f, X1)) → U49_ga(X1, maxcC_in_ga(X1))
U49_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(f, X1), X2)
U48_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(t, X1), X2)
maxcF_in_ga([]) → maxcF_out_ga([], f)
maxcF_in_ga(.(f, X1)) → U51_ga(X1, maxcF_in_ga(X1))
maxcF_in_ga(.(t, X1)) → U52_ga(X1, maxcC_in_ga(X1))
U52_ga(X1, maxcC_out_ga(X1, X2)) → maxcF_out_ga(.(t, X1), X2)
U51_ga(X1, maxcF_out_ga(X1, X2)) → maxcF_out_ga(.(f, X1), X2)
delcG_in_gga(f, X1) → delcG_out_gga(f, X1, .(f, X1))
delcG_in_gga(t, X1) → U56_gga(X1, delcJ_in_ga(X1))
delcJ_in_ga([]) → delcJ_out_ga([], [])
delcJ_in_ga(.(f, X1)) → U53_ga(X1, delcJ_in_ga(X1))
U56_gga(X1, delcJ_out_ga(X1, X2)) → delcG_out_gga(t, X1, .(f, .(f, X2)))
U53_ga(X1, delcJ_out_ga(X1, X2)) → delcJ_out_ga(.(f, X1), .(f, X2))
maxcC_in_ga(x0)
maxcF_in_ga(x0)
delcG_in_gga(x0, x1)
delcH_in_gga(x0, x1)
U48_ga(x0, x1)
U49_ga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)
U56_gga(x0, x1)
U57_gga(x0, x1)
delcJ_in_ga(x0)
U53_ga(x0, x1)
delcJ_in_ga(.(t, X1)) → delcJ_out_ga(.(t, X1), X1)
POL(.(x1, x2)) = 2·x1 + x2
POL(MAXSORTA_IN_GA(x1)) = x1
POL(U24_GA(x1, x2)) = x1
POL(U25_GA(x1, x2)) = x2
POL(U30_GA(x1, x2)) = x1 + 2·x2
POL(U31_GA(x1, x2)) = x2
POL(U48_ga(x1, x2)) = x2
POL(U49_ga(x1, x2)) = x2
POL(U51_ga(x1, x2)) = 0
POL(U52_ga(x1, x2)) = 0
POL(U53_ga(x1, x2)) = x2
POL(U56_gga(x1, x2)) = x2
POL(U57_gga(x1, x2)) = x2
POL([]) = 0
POL(delcG_in_gga(x1, x2)) = x2
POL(delcG_out_gga(x1, x2, x3)) = x3
POL(delcH_in_gga(x1, x2)) = 2·x1 + x2
POL(delcH_out_gga(x1, x2, x3)) = x3
POL(delcJ_in_ga(x1)) = x1
POL(delcJ_out_ga(x1, x2)) = x2
POL(f) = 0
POL(maxcC_in_ga(x1)) = 2
POL(maxcC_out_ga(x1, x2)) = x2
POL(maxcF_in_ga(x1)) = 1
POL(maxcF_out_ga(x1, x2)) = 0
POL(t) = 2
U24_GA(X1, maxcF_out_ga(X1, X2)) → U25_GA(X1, delcG_in_gga(X2, X1))
U25_GA(X1, delcG_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(f, .(f, X1))) → U24_GA(X1, maxcF_in_ga(X1))
MAXSORTA_IN_GA(.(f, .(t, X1))) → U30_GA(X1, maxcC_in_ga(X1))
U30_GA(X1, maxcC_out_ga(X1, X2)) → U31_GA(X1, delcH_in_gga(X2, X1))
U31_GA(X1, delcH_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
delcH_in_gga(t, X1) → U57_gga(X1, delcJ_in_ga(.(t, X1)))
U57_gga(X1, delcJ_out_ga(.(t, X1), X2)) → delcH_out_gga(t, X1, .(f, X2))
maxcC_in_ga([]) → maxcC_out_ga([], t)
maxcC_in_ga(.(t, X1)) → U48_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga(.(f, X1)) → U49_ga(X1, maxcC_in_ga(X1))
U49_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(f, X1), X2)
U48_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(t, X1), X2)
maxcF_in_ga([]) → maxcF_out_ga([], f)
maxcF_in_ga(.(f, X1)) → U51_ga(X1, maxcF_in_ga(X1))
maxcF_in_ga(.(t, X1)) → U52_ga(X1, maxcC_in_ga(X1))
U52_ga(X1, maxcC_out_ga(X1, X2)) → maxcF_out_ga(.(t, X1), X2)
U51_ga(X1, maxcF_out_ga(X1, X2)) → maxcF_out_ga(.(f, X1), X2)
delcG_in_gga(f, X1) → delcG_out_gga(f, X1, .(f, X1))
delcG_in_gga(t, X1) → U56_gga(X1, delcJ_in_ga(X1))
delcJ_in_ga([]) → delcJ_out_ga([], [])
delcJ_in_ga(.(f, X1)) → U53_ga(X1, delcJ_in_ga(X1))
U56_gga(X1, delcJ_out_ga(X1, X2)) → delcG_out_gga(t, X1, .(f, .(f, X2)))
U53_ga(X1, delcJ_out_ga(X1, X2)) → delcJ_out_ga(.(f, X1), .(f, X2))
maxcC_in_ga(x0)
maxcF_in_ga(x0)
delcG_in_gga(x0, x1)
delcH_in_gga(x0, x1)
U48_ga(x0, x1)
U49_ga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)
U56_gga(x0, x1)
U57_gga(x0, x1)
delcJ_in_ga(x0)
U53_ga(x0, x1)
U25_GA(X1, delcG_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(f, .(f, X1))) → U24_GA(X1, maxcF_in_ga(X1))
U24_GA(X1, maxcF_out_ga(X1, X2)) → U25_GA(X1, delcG_in_gga(X2, X1))
delcH_in_gga(t, X1) → U57_gga(X1, delcJ_in_ga(.(t, X1)))
U57_gga(X1, delcJ_out_ga(.(t, X1), X2)) → delcH_out_gga(t, X1, .(f, X2))
maxcC_in_ga([]) → maxcC_out_ga([], t)
maxcC_in_ga(.(t, X1)) → U48_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga(.(f, X1)) → U49_ga(X1, maxcC_in_ga(X1))
U49_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(f, X1), X2)
U48_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(t, X1), X2)
maxcF_in_ga([]) → maxcF_out_ga([], f)
maxcF_in_ga(.(f, X1)) → U51_ga(X1, maxcF_in_ga(X1))
maxcF_in_ga(.(t, X1)) → U52_ga(X1, maxcC_in_ga(X1))
U52_ga(X1, maxcC_out_ga(X1, X2)) → maxcF_out_ga(.(t, X1), X2)
U51_ga(X1, maxcF_out_ga(X1, X2)) → maxcF_out_ga(.(f, X1), X2)
delcG_in_gga(f, X1) → delcG_out_gga(f, X1, .(f, X1))
delcG_in_gga(t, X1) → U56_gga(X1, delcJ_in_ga(X1))
delcJ_in_ga([]) → delcJ_out_ga([], [])
delcJ_in_ga(.(f, X1)) → U53_ga(X1, delcJ_in_ga(X1))
U56_gga(X1, delcJ_out_ga(X1, X2)) → delcG_out_gga(t, X1, .(f, .(f, X2)))
U53_ga(X1, delcJ_out_ga(X1, X2)) → delcJ_out_ga(.(f, X1), .(f, X2))
maxcC_in_ga(x0)
maxcF_in_ga(x0)
delcG_in_gga(x0, x1)
delcH_in_gga(x0, x1)
U48_ga(x0, x1)
U49_ga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)
U56_gga(x0, x1)
U57_gga(x0, x1)
delcJ_in_ga(x0)
U53_ga(x0, x1)
U25_GA(X1, delcG_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(f, .(f, X1))) → U24_GA(X1, maxcF_in_ga(X1))
U24_GA(X1, maxcF_out_ga(X1, X2)) → U25_GA(X1, delcG_in_gga(X2, X1))
delcG_in_gga(f, X1) → delcG_out_gga(f, X1, .(f, X1))
delcG_in_gga(t, X1) → U56_gga(X1, delcJ_in_ga(X1))
delcJ_in_ga([]) → delcJ_out_ga([], [])
delcJ_in_ga(.(f, X1)) → U53_ga(X1, delcJ_in_ga(X1))
U56_gga(X1, delcJ_out_ga(X1, X2)) → delcG_out_gga(t, X1, .(f, .(f, X2)))
U53_ga(X1, delcJ_out_ga(X1, X2)) → delcJ_out_ga(.(f, X1), .(f, X2))
maxcF_in_ga([]) → maxcF_out_ga([], f)
maxcF_in_ga(.(f, X1)) → U51_ga(X1, maxcF_in_ga(X1))
maxcF_in_ga(.(t, X1)) → U52_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga([]) → maxcC_out_ga([], t)
maxcC_in_ga(.(t, X1)) → U48_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga(.(f, X1)) → U49_ga(X1, maxcC_in_ga(X1))
U52_ga(X1, maxcC_out_ga(X1, X2)) → maxcF_out_ga(.(t, X1), X2)
U49_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(f, X1), X2)
U48_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(t, X1), X2)
U51_ga(X1, maxcF_out_ga(X1, X2)) → maxcF_out_ga(.(f, X1), X2)
maxcC_in_ga(x0)
maxcF_in_ga(x0)
delcG_in_gga(x0, x1)
delcH_in_gga(x0, x1)
U48_ga(x0, x1)
U49_ga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)
U56_gga(x0, x1)
U57_gga(x0, x1)
delcJ_in_ga(x0)
U53_ga(x0, x1)
delcH_in_gga(x0, x1)
U57_gga(x0, x1)
U25_GA(X1, delcG_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(f, .(f, X1))) → U24_GA(X1, maxcF_in_ga(X1))
U24_GA(X1, maxcF_out_ga(X1, X2)) → U25_GA(X1, delcG_in_gga(X2, X1))
delcG_in_gga(f, X1) → delcG_out_gga(f, X1, .(f, X1))
delcG_in_gga(t, X1) → U56_gga(X1, delcJ_in_ga(X1))
delcJ_in_ga([]) → delcJ_out_ga([], [])
delcJ_in_ga(.(f, X1)) → U53_ga(X1, delcJ_in_ga(X1))
U56_gga(X1, delcJ_out_ga(X1, X2)) → delcG_out_gga(t, X1, .(f, .(f, X2)))
U53_ga(X1, delcJ_out_ga(X1, X2)) → delcJ_out_ga(.(f, X1), .(f, X2))
maxcF_in_ga([]) → maxcF_out_ga([], f)
maxcF_in_ga(.(f, X1)) → U51_ga(X1, maxcF_in_ga(X1))
maxcF_in_ga(.(t, X1)) → U52_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga([]) → maxcC_out_ga([], t)
maxcC_in_ga(.(t, X1)) → U48_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga(.(f, X1)) → U49_ga(X1, maxcC_in_ga(X1))
U52_ga(X1, maxcC_out_ga(X1, X2)) → maxcF_out_ga(.(t, X1), X2)
U49_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(f, X1), X2)
U48_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(t, X1), X2)
U51_ga(X1, maxcF_out_ga(X1, X2)) → maxcF_out_ga(.(f, X1), X2)
maxcC_in_ga(x0)
maxcF_in_ga(x0)
delcG_in_gga(x0, x1)
U48_ga(x0, x1)
U49_ga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)
U56_gga(x0, x1)
delcJ_in_ga(x0)
U53_ga(x0, x1)
delcG_in_gga(t, X1) → U56_gga(X1, delcJ_in_ga(X1))
POL(.(x1, x2)) = 2·x1 + 2·x2
POL(MAXSORTA_IN_GA(x1)) = x1
POL(U24_GA(x1, x2)) = 2·x1 + x2
POL(U25_GA(x1, x2)) = x2
POL(U48_ga(x1, x2)) = x2
POL(U49_ga(x1, x2)) = x2
POL(U51_ga(x1, x2)) = 2·x2
POL(U52_ga(x1, x2)) = 2·x2
POL(U53_ga(x1, x2)) = 2·x2
POL(U56_gga(x1, x2)) = 2·x2
POL([]) = 0
POL(delcG_in_gga(x1, x2)) = 2·x1 + 2·x2
POL(delcG_out_gga(x1, x2, x3)) = x3
POL(delcJ_in_ga(x1)) = 0
POL(delcJ_out_ga(x1, x2)) = 2·x2
POL(f) = 0
POL(maxcC_in_ga(x1)) = 2
POL(maxcC_out_ga(x1, x2)) = x2
POL(maxcF_in_ga(x1)) = x1
POL(maxcF_out_ga(x1, x2)) = 2·x2
POL(t) = 2
U25_GA(X1, delcG_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(f, .(f, X1))) → U24_GA(X1, maxcF_in_ga(X1))
U24_GA(X1, maxcF_out_ga(X1, X2)) → U25_GA(X1, delcG_in_gga(X2, X1))
delcG_in_gga(f, X1) → delcG_out_gga(f, X1, .(f, X1))
delcJ_in_ga([]) → delcJ_out_ga([], [])
delcJ_in_ga(.(f, X1)) → U53_ga(X1, delcJ_in_ga(X1))
U56_gga(X1, delcJ_out_ga(X1, X2)) → delcG_out_gga(t, X1, .(f, .(f, X2)))
U53_ga(X1, delcJ_out_ga(X1, X2)) → delcJ_out_ga(.(f, X1), .(f, X2))
maxcF_in_ga([]) → maxcF_out_ga([], f)
maxcF_in_ga(.(f, X1)) → U51_ga(X1, maxcF_in_ga(X1))
maxcF_in_ga(.(t, X1)) → U52_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga([]) → maxcC_out_ga([], t)
maxcC_in_ga(.(t, X1)) → U48_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga(.(f, X1)) → U49_ga(X1, maxcC_in_ga(X1))
U52_ga(X1, maxcC_out_ga(X1, X2)) → maxcF_out_ga(.(t, X1), X2)
U49_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(f, X1), X2)
U48_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(t, X1), X2)
U51_ga(X1, maxcF_out_ga(X1, X2)) → maxcF_out_ga(.(f, X1), X2)
maxcC_in_ga(x0)
maxcF_in_ga(x0)
delcG_in_gga(x0, x1)
U48_ga(x0, x1)
U49_ga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)
U56_gga(x0, x1)
delcJ_in_ga(x0)
U53_ga(x0, x1)
U25_GA(X1, delcG_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(f, .(f, X1))) → U24_GA(X1, maxcF_in_ga(X1))
U24_GA(X1, maxcF_out_ga(X1, X2)) → U25_GA(X1, delcG_in_gga(X2, X1))
delcG_in_gga(f, X1) → delcG_out_gga(f, X1, .(f, X1))
maxcF_in_ga([]) → maxcF_out_ga([], f)
maxcF_in_ga(.(f, X1)) → U51_ga(X1, maxcF_in_ga(X1))
maxcF_in_ga(.(t, X1)) → U52_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga([]) → maxcC_out_ga([], t)
maxcC_in_ga(.(t, X1)) → U48_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga(.(f, X1)) → U49_ga(X1, maxcC_in_ga(X1))
U52_ga(X1, maxcC_out_ga(X1, X2)) → maxcF_out_ga(.(t, X1), X2)
U49_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(f, X1), X2)
U48_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(t, X1), X2)
U51_ga(X1, maxcF_out_ga(X1, X2)) → maxcF_out_ga(.(f, X1), X2)
maxcC_in_ga(x0)
maxcF_in_ga(x0)
delcG_in_gga(x0, x1)
U48_ga(x0, x1)
U49_ga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)
U56_gga(x0, x1)
delcJ_in_ga(x0)
U53_ga(x0, x1)
U56_gga(x0, x1)
delcJ_in_ga(x0)
U53_ga(x0, x1)
U25_GA(X1, delcG_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(f, .(f, X1))) → U24_GA(X1, maxcF_in_ga(X1))
U24_GA(X1, maxcF_out_ga(X1, X2)) → U25_GA(X1, delcG_in_gga(X2, X1))
delcG_in_gga(f, X1) → delcG_out_gga(f, X1, .(f, X1))
maxcF_in_ga([]) → maxcF_out_ga([], f)
maxcF_in_ga(.(f, X1)) → U51_ga(X1, maxcF_in_ga(X1))
maxcF_in_ga(.(t, X1)) → U52_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga([]) → maxcC_out_ga([], t)
maxcC_in_ga(.(t, X1)) → U48_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga(.(f, X1)) → U49_ga(X1, maxcC_in_ga(X1))
U52_ga(X1, maxcC_out_ga(X1, X2)) → maxcF_out_ga(.(t, X1), X2)
U49_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(f, X1), X2)
U48_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(t, X1), X2)
U51_ga(X1, maxcF_out_ga(X1, X2)) → maxcF_out_ga(.(f, X1), X2)
maxcC_in_ga(x0)
maxcF_in_ga(x0)
delcG_in_gga(x0, x1)
U48_ga(x0, x1)
U49_ga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)
U24_GA(x0, maxcF_out_ga(x0, f)) → U25_GA(x0, delcG_out_gga(f, x0, .(f, x0)))
U25_GA(X1, delcG_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(f, .(f, X1))) → U24_GA(X1, maxcF_in_ga(X1))
U24_GA(x0, maxcF_out_ga(x0, f)) → U25_GA(x0, delcG_out_gga(f, x0, .(f, x0)))
delcG_in_gga(f, X1) → delcG_out_gga(f, X1, .(f, X1))
maxcF_in_ga([]) → maxcF_out_ga([], f)
maxcF_in_ga(.(f, X1)) → U51_ga(X1, maxcF_in_ga(X1))
maxcF_in_ga(.(t, X1)) → U52_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga([]) → maxcC_out_ga([], t)
maxcC_in_ga(.(t, X1)) → U48_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga(.(f, X1)) → U49_ga(X1, maxcC_in_ga(X1))
U52_ga(X1, maxcC_out_ga(X1, X2)) → maxcF_out_ga(.(t, X1), X2)
U49_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(f, X1), X2)
U48_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(t, X1), X2)
U51_ga(X1, maxcF_out_ga(X1, X2)) → maxcF_out_ga(.(f, X1), X2)
maxcC_in_ga(x0)
maxcF_in_ga(x0)
delcG_in_gga(x0, x1)
U48_ga(x0, x1)
U49_ga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)
U25_GA(X1, delcG_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(f, .(f, X1))) → U24_GA(X1, maxcF_in_ga(X1))
U24_GA(x0, maxcF_out_ga(x0, f)) → U25_GA(x0, delcG_out_gga(f, x0, .(f, x0)))
maxcF_in_ga([]) → maxcF_out_ga([], f)
maxcF_in_ga(.(f, X1)) → U51_ga(X1, maxcF_in_ga(X1))
maxcF_in_ga(.(t, X1)) → U52_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga([]) → maxcC_out_ga([], t)
maxcC_in_ga(.(t, X1)) → U48_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga(.(f, X1)) → U49_ga(X1, maxcC_in_ga(X1))
U52_ga(X1, maxcC_out_ga(X1, X2)) → maxcF_out_ga(.(t, X1), X2)
U49_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(f, X1), X2)
U48_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(t, X1), X2)
U51_ga(X1, maxcF_out_ga(X1, X2)) → maxcF_out_ga(.(f, X1), X2)
maxcC_in_ga(x0)
maxcF_in_ga(x0)
delcG_in_gga(x0, x1)
U48_ga(x0, x1)
U49_ga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)
delcG_in_gga(x0, x1)
U25_GA(X1, delcG_out_gga(X2, X1, X4)) → MAXSORTA_IN_GA(X4)
MAXSORTA_IN_GA(.(f, .(f, X1))) → U24_GA(X1, maxcF_in_ga(X1))
U24_GA(x0, maxcF_out_ga(x0, f)) → U25_GA(x0, delcG_out_gga(f, x0, .(f, x0)))
maxcF_in_ga([]) → maxcF_out_ga([], f)
maxcF_in_ga(.(f, X1)) → U51_ga(X1, maxcF_in_ga(X1))
maxcF_in_ga(.(t, X1)) → U52_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga([]) → maxcC_out_ga([], t)
maxcC_in_ga(.(t, X1)) → U48_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga(.(f, X1)) → U49_ga(X1, maxcC_in_ga(X1))
U52_ga(X1, maxcC_out_ga(X1, X2)) → maxcF_out_ga(.(t, X1), X2)
U49_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(f, X1), X2)
U48_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(t, X1), X2)
U51_ga(X1, maxcF_out_ga(X1, X2)) → maxcF_out_ga(.(f, X1), X2)
maxcC_in_ga(x0)
maxcF_in_ga(x0)
U48_ga(x0, x1)
U49_ga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)
U25_GA(z0, delcG_out_gga(f, z0, .(f, z0))) → MAXSORTA_IN_GA(.(f, z0))
MAXSORTA_IN_GA(.(f, .(f, X1))) → U24_GA(X1, maxcF_in_ga(X1))
U24_GA(x0, maxcF_out_ga(x0, f)) → U25_GA(x0, delcG_out_gga(f, x0, .(f, x0)))
U25_GA(z0, delcG_out_gga(f, z0, .(f, z0))) → MAXSORTA_IN_GA(.(f, z0))
maxcF_in_ga([]) → maxcF_out_ga([], f)
maxcF_in_ga(.(f, X1)) → U51_ga(X1, maxcF_in_ga(X1))
maxcF_in_ga(.(t, X1)) → U52_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga([]) → maxcC_out_ga([], t)
maxcC_in_ga(.(t, X1)) → U48_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga(.(f, X1)) → U49_ga(X1, maxcC_in_ga(X1))
U52_ga(X1, maxcC_out_ga(X1, X2)) → maxcF_out_ga(.(t, X1), X2)
U49_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(f, X1), X2)
U48_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(t, X1), X2)
U51_ga(X1, maxcF_out_ga(X1, X2)) → maxcF_out_ga(.(f, X1), X2)
maxcC_in_ga(x0)
maxcF_in_ga(x0)
U48_ga(x0, x1)
U49_ga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)
MAXSORTA_IN_GA(.(f, .(f, X1))) → U24_GA(X1, maxcF_in_ga(X1))
U24_GA(x0, maxcF_out_ga(x0, f)) → U25_GA(x0, delcG_out_gga(f, x0, .(f, x0)))
U25_GA(z0, delcG_out_gga(f, z0, .(f, z0))) → MAXSORTA_IN_GA(.(f, z0))
POL(.(x1, x2)) = 1 + 2·x1 + 2·x2
POL(MAXSORTA_IN_GA(x1)) = 2·x1
POL(U24_GA(x1, x2)) = 1 + x1 + 2·x2
POL(U25_GA(x1, x2)) = 2 + x1 + x2
POL(U48_ga(x1, x2)) = 1 + x1 + x2
POL(U49_ga(x1, x2)) = 1 + x1 + x2
POL(U51_ga(x1, x2)) = 2 + 2·x1 + x2
POL(U52_ga(x1, x2)) = 2 + 2·x1 + 2·x2
POL([]) = 0
POL(delcG_out_gga(x1, x2, x3)) = x1 + 2·x2 + x3
POL(f) = 0
POL(maxcC_in_ga(x1)) = 1 + x1
POL(maxcC_out_ga(x1, x2)) = 1 + x1 + 2·x2
POL(maxcF_in_ga(x1)) = 2 + 2·x1
POL(maxcF_out_ga(x1, x2)) = 2 + 2·x1 + 2·x2
POL(t) = 0
maxcF_in_ga([]) → maxcF_out_ga([], f)
maxcF_in_ga(.(f, X1)) → U51_ga(X1, maxcF_in_ga(X1))
maxcF_in_ga(.(t, X1)) → U52_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga([]) → maxcC_out_ga([], t)
maxcC_in_ga(.(t, X1)) → U48_ga(X1, maxcC_in_ga(X1))
maxcC_in_ga(.(f, X1)) → U49_ga(X1, maxcC_in_ga(X1))
U52_ga(X1, maxcC_out_ga(X1, X2)) → maxcF_out_ga(.(t, X1), X2)
U49_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(f, X1), X2)
U48_ga(X1, maxcC_out_ga(X1, X2)) → maxcC_out_ga(.(t, X1), X2)
U51_ga(X1, maxcF_out_ga(X1, X2)) → maxcF_out_ga(.(f, X1), X2)
maxcC_in_ga(x0)
maxcF_in_ga(x0)
U48_ga(x0, x1)
U49_ga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)